CVC4:如何获得正确的非卫星核心？

Question

使用此代码：

#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;
}

我得到以下答复：

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

但我希望这样的事情：

unsat (qr rs nqs )

我假设，参数inUnsatCore of SmtEngine.assertFormula会以某种方式引导断言。但事实并非如此。

什么是正确的方式断言公式和要求一个非卫星核心，如果不像上面所示？

使用带有github标签1.5的cvc4版本。

Answer 1

qr rs nqs本身并不是一个unsat核心(通过将所有三个变量都设置为true，它是可以满足的)。似乎您正在尝试实现类似于SMT v2中的命名断言。在SMT v2中使用v2时，只打印出unsat核心中的命名断言。

您的示例可翻译如下：

(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 4在本例中的输出：

unsat
(
_nqs
_rs
_qr
)

这在内部的工作方式是，CVC4跟踪命名断言，并且只打印出这些断言，而忽略未命名的断言。如果unsat核心的成员属于您的相关断言集(pq、qr、rs、st、nqs)，则可以在代码中进行同样的操作。

据我所知，inUnsatCore在produce-unsat-cores是true时没有效果。我在维护列表中添加了一个改进文档的项目。