CVC4: How to get proper unsat core?

Question

Using this code:

#include <cvc4/cvc4.h>

using namespace std;
using namespace CVC4;

int main() {
  ExprManager em;
  SmtEngine smt(&em);
  smt.setOption("produce-unsat-cores","true");

  Type boolean_type = em.booleanType();

  Expr p = em.mkVar("p", boolean_type);
  Expr q = em.mkVar("q", boolean_type);
  Expr r = em.mkVar("r", boolean_type);
  Expr s = em.mkVar("s", boolean_type);
  Expr t = em.mkVar("t", boolean_type);

  Expr pq = em.mkVar("pq", boolean_type);
  Expr qr = em.mkVar("qr", boolean_type);
  Expr rs = em.mkVar("rs", boolean_type);
  Expr st = em.mkVar("st", boolean_type);
  Expr nqs = em.mkVar("nqs", boolean_type);

  smt.assertFormula(em.mkExpr(kind::IMPLIES, pq, em.mkExpr(kind::IMPLIES, p, q)),false);
  smt.assertFormula(em.mkExpr(kind::IMPLIES, qr, em.mkExpr(kind::IMPLIES, q, r)),false);
  smt.assertFormula(em.mkExpr(kind::IMPLIES, rs, em.mkExpr(kind::IMPLIES, r, s)),false);
  smt.assertFormula(em.mkExpr(kind::IMPLIES, st, em.mkExpr(kind::IMPLIES, s, t)),false);
  smt.assertFormula(em.mkExpr(kind::IMPLIES, nqs, em.mkExpr(kind::NOT, em.mkExpr(kind::IMPLIES, q, s))),false);

  smt.assertFormula(pq,true);
  smt.assertFormula(qr,true);
  smt.assertFormula(rs,true);
  smt.assertFormula(st,true);
  smt.assertFormula(nqs,true);

  Result result = smt.checkSat();
  enum Result::Sat sat_result = result.isSat();
  if (sat_result == Result::SAT) {
    printf("sat\n");
  } else if (sat_result == Result::UNSAT) {
    printf("unsat (");
    UnsatCore unsat_core = smt.getUnsatCore();
    std::vector<Expr>::const_iterator it = unsat_core.begin();
    std::vector<Expr>::const_iterator it_end = unsat_core.end();
    for (; it != it_end; ++it) {
      printf("%s ", Expr(*it).toString().c_str());
    }
    printf(")\n");
  } else {
    printf("unknown\n");
  }

  return 0;
}

I get the following response:

unsat (qr rs nqs qr => (q => r) rs => (r => s) nqs => NOT(q => s) )

But I would expect something like:

unsat (qr rs nqs )

I assumed, that the parameter inUnsatCore of SmtEngine.assertFormula would direct the assertions in that way somehow. But it does not.

What is the correct way of asserting formulas and asking for an unsat core, if not like shown above?

Using a cvc4 version with the tag 1.5 from github.

Answer 1

qr rs nqs is not an unsat core per se (it is trivially satisfiable by setting all three variables to true). It seems like you are trying to achieve something similar to named assertions in SMT-LIB v2. When using (get-unsat-core) in SMT-LIB v2, only named assertions in the unsat core are printed.

Your example could be translated as follows:

(set-option :produce-unsat-cores true)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Bool)
(declare-fun pq () Bool)
(declare-fun qr () Bool)
(declare-fun rs () Bool)
(declare-fun st () Bool)
(declare-fun nqs () Bool)
(assert (implies pq (implies p q)))
(assert (implies qr (implies q r)))
(assert (implies rs (implies r s)))
(assert (implies st (implies s t)))
(assert (implies nqs (not (implies q s))))
(assert (! pq :named _pq))
(assert (! qr :named _qr))
(assert (! rs :named _rs))
(assert (! st :named _st))
(assert (! nqs :named _nqs))
(check-sat)
(get-unsat-core)

CVC4's output on this example:

unsat
(
_nqs
_rs
_qr
)

The way this works internally is that CVC4 keeps track of named assertions and only prints those out while skipping unnamed ones. You could do the same in your code by only printing members of the unsat core if they belong to your set of relevant assertions (pq, qr, rs, st, nqs).

inUnsatCore has no effect when produce-unsat-cores is true as far as I can tell. I've added an item for improving that documentation to our maintenance list.