SMTLib2 Output Consistency for Quantified Terms

[baierd]

I noticed that quantified formulas are dumped in many different ways, some of which are inconsistent with SMTLib2 and can not be parsed by other solvers.

We should add I/O tests for quantified terms and report or fix inconsistent output.

An basic example implementation could be based of these 2 tests:

  @Test
  public void quantifierIntegerDumpTest() {
    requireIntegers();
    requireQuantifiers();

    IntegerFormula int1 = imgr.makeNumber(1);
    IntegerFormula var = imgr.makeVariable("var_a");
    BooleanFormula body = imgr.equal(int1, var);
    BooleanFormula formula = qmgr.forall(var, body);

    String formDump = mgr.dumpFormula(formula).toString();

    // check that function is dumped correctly + necessary assert that has to be there
    assertThat(formDump).contains("(assert (forall ((var_a Int)) (= 1 var_a)))");
    checkThatAssertIsInLastLine(formDump);
    checkThatDumpIsParseable(formDump);
  }

  @Test
  public void quantifierBitvectorDumpTest() {
    requireBitvectors();
    requireQuantifiers();

    BitvectorFormula int1 = bvmgr.makeBitvector(8, 1);
    BitvectorFormula var = bvmgr.makeVariable(8, "var_a");
    BooleanFormula body = bvmgr.equal(int1, var);
    BooleanFormula formula = qmgr.forall(var, body);

    String formDump = mgr.dumpFormula(formula).toString();

    // check that function is dumped correctly + necessary assert that has to be there
    assertThat(formDump).contains("(assert (forall ((var_a (_ BitVec 8))) (= #b00000001 var_a)))");
    checkThatAssertIsInLastLine(formDump);
    checkThatDumpIsParseable(formDump);
  }

[daniel-raffler]

I noticed that quantified formulas are dumped in many different ways, some of which are inconsistent with SMTLib2 and can not be parsed by other solvers.

If this is about Yices, it actually uses it's own input language (here) when printing formulas. The output is similar enough to SMTLIB to get away with it most of the time, but sometimes it will break. See also this issue.

[kfriedberger]

For quantified formulas, solvers have subtle differences when dumping SMTLIB, for example:

// formula: (FORALL (x Int) (= 1 x))
switch (solverToUse()) {
  case Z3:
    return "(assert (forall ((x Int)) (! (= 1 x) :weight 0)))\n"; // with weight
  case PRINCESS:
    return "(assert (forall ((var0 Int)) (= 1 var0)))\n"; // renamed symbols
  case CVC4:
    return "(assert (forall ((x Int)) (= 1 x) ))\n"; // with trailing space
  case YICES2:
    return "(assert (forall (x::int) (= 1 x)))\n"; // special type annotation
  default: // other solvers
    return "(assert (forall ((x Int)) (= 1 x)))\n"; // normal
}

While renamed symbols and whitespace is valid SMTLIB and irrelevant (maybe inconvenient for the user),
the added weight of Z3 is a special case for Z3 (but also acceptable).
The main issue is Yices with its special type notation.