Unsat-Core extraction with CVC 4

[mikand]

Currently, the pysmt wrapper of CVC4 does not support unsat core extraction. If this feature is supported by the solver (unclear), we should add it to our wrapper.

[marcogario]

The following snippet shows the support for Unsat Core.

def demo_ucore_cvc4():
        x = Symbol("x")
        with Solver(name="cvc4",
                    solver_options={'produce-unsat-cores': "true"}) as s:
            s.add_assertion(x)
            s.add_assertion(Not(x))
            r = s.solve()
            self.assertFalse(r)

            core = s.get_unsat_core()
            print(core)

Note:

1. Option produce-unsat-cores must be set;
2. The returned object is an UnsatCore class, that can be iterated upon to extract the elements of the core. However, the wrapper seems to be pretty rough, and some python glue might be needed. This is an example from smt_engine.cpp:

  for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
    Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;
    coreChecker.assertFormula(*i);
  }