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.