Expose API to convert solver into SMT-LIB2 format

[108anup]

Hi, I was unable to find a function that converts the solver to SMT-LIB2 format. I wrote one based on the functions in the python/C++ APIs below.

    def to_smt2(self):
        """return SMTLIB2 formatted benchmark for solver's assertions"""
        es = self.assertionsassertions()
        sz = len(es)
        sz1 = sz
        if sz1 > 0:
            sz1 -= 1
        v = (Ast * sz1)()
        for i in range(sz1):
            v[i] = es[i].as_ast()
        if sz > 0:
            e = es[sz1].as_ast()
        else:
            e = BoolVal(True, self.ctxctx).as_ast()
        return Z3_benchmark_to_smtlib_string(
            self.ctxctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
        )

    std::string to_smt2(char const* status = "unknown") {
        array<Z3_ast> es(assertions());
        Z3_ast const* fmls = es.ptr();
        Z3_ast fml = 0;
        unsigned sz = es.size();
        if (sz > 0) {
            --sz;
            fml = fmls[sz];
        }
        else {
            fml = ctx().bool_val(true);
        }
        return std::string(Z3_benchmark_to_smtlib_string(
                               ctx(),
                               "", "", status, "",
                               sz,
                               fmls,
                               fml));
    }

[108anup]

One simple test is:

#[test]
fn test_solver_to_smtlib2() {
    let cfg = Config::new();
    let ctx = Context::new(&cfg);
    let solver = Solver::new(&ctx);
    let t1 = ast::Bool::from_bool(&ctx, true);
    let t2 = ast::Bool::from_bool(&ctx, true);
    solver.assert(&t1._eq(&t2));
    println!("{}", solver.to_smt2());
    let expected = r#"; benchmark generated from rust API
(set-info :status unknown)
(assert
 (= true true))
(check-sat)
"#;
    assert_eq!(solver.to_smt2(), expected);
}

But this hardcodes string matching which may be fragile. Another test is:

#[test]
fn test_solver_to_smtlib2() {
    let cfg = Config::new();
    let ctx = Context::new(&cfg);
    let solver1 = Solver::new(&ctx);
    let t1 = ast::Bool::from_bool(&ctx, true);
    let t2 = ast::Bool::from_bool(&ctx, true);
    solver1.assert(&t1._eq(&t2));
    let s1_smt2 = solver1.to_smt2();
    let solver2 = Solver::new(&ctx);
    solver2.from_string(s1_smt2);
    assert_eq!(solver2.check(), solver1.check());
}

But this one does not explicitly check if the output smt2 is legit, only that its truth value matches. But this test is similar to the one for smt2 to solver test. So I raised PR with this test.

LMK if you had some other test in mind.

[waywardmonkeys]

Thanks!