Remove "inUnsatCore" flag throughout (#6964)

The internal solver no longer cares about what assertions are named / are in the unsat core.

This simplifies the code so that the (now unused) `inUnsatCore` flag is removed from all interfaces.

This eliminates another external use of `getSmtEngine`.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 483da3ff0e287f91fe2b8e2fe38868ea4e3cb3eb..f56fc3c90159ad19e58c17a958cb7e57dcfa1cd9 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -359,9 +359,9 @@ command [std::unique_ptr<cvc5::Command>* cmd]
     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { PARSER_STATE->clearLastNamedTerm(); }
     term[expr, expr2]
-    { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
-      cmd->reset(new AssertCommand(expr, inUnsatCore));
-      if(inUnsatCore) {
+    { cmd->reset(new AssertCommand(expr));
+      if (PARSER_STATE->lastNamedTerm().first == expr)
+      {
         // set the expression name, if there was a named term
         std::pair<api::Term, std::string> namedTerm =
             PARSER_STATE->lastNamedTerm();

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index c96fbf07db3c9367d33c9bdea610b550f8a7b714..feaf876f73db3d65f58a7342b0051c939c0747bb 100644 (file)
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -165,7 +165,7 @@ parseCommand returns [cvc5::Command* cmd = NULL]
         SYM_MAN->setExpressionName(aexpr, name, true);
       }
       // make the command to assert the formula
-      cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ true, true);
+      cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, true);
     }
   | FOF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
     { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(true); }
@@ -177,7 +177,7 @@ parseCommand returns [cvc5::Command* cmd = NULL]
         SYM_MAN->setExpressionName(aexpr, name, true);
       }
       // make the command to assert the formula
-      cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
+      cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, false);
     }
   | TFF_TOK LPAREN_TOK nameN[name] COMMA_TOK
     ( TYPE_TOK COMMA_TOK tffTypedAtom[cmd]
@@ -191,7 +191,7 @@ parseCommand returns [cvc5::Command* cmd = NULL]
           SYM_MAN->setExpressionName(aexpr, name, true);
         }
         // make the command to assert the formula
-        cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
+        cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, false);
       }
     ) RPAREN_TOK DOT_TOK
   | THF_TOK
@@ -218,8 +218,7 @@ parseCommand returns [cvc5::Command* cmd = NULL]
           SYM_MAN->setExpressionName(aexpr, name, true);
         }
         // make the command to assert the formula
-        cmd = PARSER_STATE->makeAssertCommand(
-            fr, aexpr, /* cnf == */ false, true);
+        cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, false);
       }
     ) RPAREN_TOK DOT_TOK
   | INCLUDE_TOK LPAREN_TOK unquotedFileName[name]
@@ -249,7 +248,7 @@ parseCommand returns [cvc5::Command* cmd = NULL]
       cvc5::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants();
       if( !aexpr.isNull() )
       {
-        seq->addCommand(new AssertCommand(aexpr, false));
+        seq->addCommand(new AssertCommand(aexpr));
       }
 
       std::string filename = PARSER_STATE->getInput()->getInputStreamName();

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 91fcc7a12eaa2110ce731ff98d556626fdc8d858..7c65f5c57f390fc8a355aba9058ce18a08f176d3 100644 (file)
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -573,10 +573,7 @@ api::Term Tptp::getAssertionDistinctConstants()
   return d_nullExpr;
 }
 
-Command* Tptp::makeAssertCommand(FormulaRole fr,
-                                 api::Term expr,
-                                 bool cnf,
-                                 bool inUnsatCore)
+Command* Tptp::makeAssertCommand(FormulaRole fr, api::Term expr, bool cnf)
 {
   // For SZS ontology compliance.
   // if we're in cnf() though, conjectures don't result in "Theorem" or
@@ -588,7 +585,7 @@ Command* Tptp::makeAssertCommand(FormulaRole fr,
   if( expr.isNull() ){
     return new EmptyCommand("Untreated role for expression");
   }else{
-    return new AssertCommand(expr, inUnsatCore);
+    return new AssertCommand(expr);
   }
 }
 

diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 258394486838fd0973137a8998bb7fe1e3f3b78b..2167a6c3898a925c628930d1801d49ca90510ae5 100644 (file)
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -134,10 +134,7 @@ class Tptp : public Parser {
    * getAssertionExpr above). This may set a flag in the parser to mark
    * that we have asserted a conjecture.
    */
-  Command* makeAssertCommand(FormulaRole fr,
-                             api::Term expr,
-                             bool cnf,
-                             bool inUnsatCore);
+  Command* makeAssertCommand(FormulaRole fr, api::Term expr, bool cnf);
 
   /** Ugly hack because I don't know how to return an expression from a
       token */

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 504dce71e7b6d2a1d5642a52f2f1290af22dcc84..b7688d833eb2729567e5da29b33b09d4aa58efe3 100644 (file)
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -70,7 +70,6 @@ void Assertions::clearCurrent()
 }
 
 void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
-                                    bool inUnsatCore,
                                     bool isEntailmentCheck)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -105,7 +104,7 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
     Node n = d_absValues.substituteAbstractValues(e);
     // Ensure expr is type-checked at this point.
     ensureBoolean(n);
-    addFormula(n, inUnsatCore, true, true, false, false);
+    addFormula(n, true, true, false, false);
   }
   if (d_globalDefineFunLemmas != nullptr)
   {
@@ -114,16 +113,16 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
     // zero assertions)
     for (const Node& lemma : *d_globalDefineFunLemmas)
     {
-      addFormula(lemma, false, true, false, true, false);
+      addFormula(lemma, true, false, true, false);
     }
   }
 }
 
-void Assertions::assertFormula(const Node& n, bool inUnsatCore)
+void Assertions::assertFormula(const Node& n)
 {
   ensureBoolean(n);
   bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
-  addFormula(n, inUnsatCore, true, false, false, maybeHasFv);
+  addFormula(n, true, false, false, maybeHasFv);
 }
 
 std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
@@ -141,7 +140,6 @@ context::CDList<Node>* Assertions::getAssertionList()
 }
 
 void Assertions::addFormula(TNode n,
-                            bool inUnsatCore,
                             bool inInput,
                             bool isAssumption,
                             bool isFunDef,
@@ -158,7 +156,6 @@ void Assertions::addFormula(TNode n,
     return;
   }
   Trace("smt") << "SmtEnginePrivate::addFormula(" << n
-               << "), inUnsatCore = " << inUnsatCore
                << ", inInput = " << inInput
                << ", isAssumption = " << isAssumption
                << ", isFunDef = " << isFunDef << std::endl;
@@ -210,7 +207,7 @@ void Assertions::addDefineFunDefinition(Node n, bool global)
   {
     // we don't check for free variables here, since even if we are sygus,
     // we could contain functions-to-synthesize within definitions.
-    addFormula(n, false, true, false, true, false);
+    addFormula(n, true, false, true, false);
   }
 }
 

diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index c922cbaea7c9fa3c97d4564502a8f342c14cad72..de7ba72c9260762b2733aad3ce01fa34b5ce106d 100644 (file)
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -65,24 +65,20 @@ class Assertions
    * upcoming check-sat call.
    *
    * @param assumptions The assumptions of the upcoming check-sat call.
-   * @param inUnsatCore Whether assumptions are in the unsat core.
    * @param isEntailmentCheck Whether we are checking entailment of assumptions
    * in the upcoming check-sat call.
    */
   void initializeCheckSat(const std::vector<Node>& assumptions,
-                          bool inUnsatCore,
                           bool isEntailmentCheck);
   /**
    * Add a formula to the current context: preprocess, do per-theory
    * setup, use processAssertionList(), asserting to T-solver for
    * literals and conjunction of literals.  Returns false if
-   * immediately determined to be inconsistent.  This version
-   * takes a Boolean flag to determine whether to include this asserted
-   * formula in an unsat core (if one is later requested).
+   * immediately determined to be inconsistent.
    *
    * @throw TypeCheckingException, LogicException, UnsafeInterruptException
    */
-  void assertFormula(const Node& n, bool inUnsatCore = true);
+  void assertFormula(const Node& n);
   /**
    * Assert that n corresponds to an assertion from a define-fun or
    * define-fun-rec command.
@@ -145,7 +141,6 @@ class Assertions
    * (this is used to distinguish assertions and assumptions)
    */
   void addFormula(TNode n,
-                  bool inUnsatCore,
                   bool inInput,
                   bool isAssumption,
                   bool isFunDef,

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 5f0da7a0c4e132c70ab05410c3c82bb280227efd..36bc170965ec704d850d0501229888044d5a8086 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -343,17 +343,14 @@ void EchoCommand::toStream(std::ostream& out,
 /* class AssertCommand                                                        */
 /* -------------------------------------------------------------------------- */
 
-AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore)
-    : d_term(t), d_inUnsatCore(inUnsatCore)
-{
-}
+AssertCommand::AssertCommand(const api::Term& t) : d_term(t) {}
 
 api::Term AssertCommand::getTerm() const { return d_term; }
 void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    solver->getSmtEngine()->assertFormula(termToNode(d_term), d_inUnsatCore);
+    solver->assertFormula(d_term);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (UnsafeInterruptException& e)
@@ -366,10 +363,7 @@ void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* AssertCommand::clone() const
-{
-  return new AssertCommand(d_term, d_inUnsatCore);
-}
+Command* AssertCommand::clone() const { return new AssertCommand(d_term); }
 
 std::string AssertCommand::getCommandName() const { return "assert"; }
 
@@ -581,10 +575,7 @@ void CheckSatAssumingCommand::toStream(std::ostream& out,
 /* class QueryCommand                                                         */
 /* -------------------------------------------------------------------------- */
 
-QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore)
-    : d_term(t), d_inUnsatCore(inUnsatCore)
-{
-}
+QueryCommand::QueryCommand(const api::Term& t) : d_term(t) {}
 
 api::Term QueryCommand::getTerm() const { return d_term; }
 void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm)
@@ -615,7 +606,7 @@ void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
 
 Command* QueryCommand::clone() const
 {
-  QueryCommand* c = new QueryCommand(d_term, d_inUnsatCore);
+  QueryCommand* c = new QueryCommand(d_term);
   c->d_result = d_result;
   return c;
 }

diff --git a/src/smt/command.h b/src/smt/command.h
index 2d32062e207af133f42201eb103b09a4f085aafe..590fcace3c38cf4a5ea2d2dad5ff570495156aa4 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -348,10 +348,9 @@ class CVC5_EXPORT AssertCommand : public Command
 {
  protected:
   api::Term d_term;
-  bool d_inUnsatCore;
 
  public:
-  AssertCommand(const api::Term& t, bool inUnsatCore = true);
+  AssertCommand(const api::Term& t);
 
   api::Term getTerm() const;
 
@@ -706,10 +705,9 @@ class CVC5_EXPORT QueryCommand : public Command
  protected:
   api::Term d_term;
   api::Result d_result;
-  bool d_inUnsatCore;
 
  public:
-  QueryCommand(const api::Term& t, bool inUnsatCore = true);
+  QueryCommand(const api::Term& t);
 
   api::Term getTerm() const;
   api::Result getResult() const;

diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index e66717f5b77858e2678d41388467e7bc55647711..185a60e46252055c6e4a6ba6e1714dd9b2e1bf17 100644 (file)
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -75,8 +75,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
   Assert(ne.getNumChildren() == 3);
   // We consider this to be an entailment check, which also avoids incorrect
   // status reporting (see SmtEngineState::d_expectedStatus).
-  Result r =
-      d_smtSolver.checkSatisfiability(as, std::vector<Node>{ne}, false, true);
+  Result r = d_smtSolver.checkSatisfiability(as, std::vector<Node>{ne}, true);
   Trace("smt-qe") << "Query returned " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
   {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b9ed95339fcc23554eec17a2d7c895e335e16647..774d8b19247e82a1091efb590caf3b036bebd9c3 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -831,7 +831,7 @@ Result SmtEngine::checkSat()
   return checkSat(nullNode);
 }
 
-Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore)
+Result SmtEngine::checkSat(const Node& assumption)
 {
   if (Dump.isOn("benchmark"))
   {
@@ -843,11 +843,10 @@ Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore)
   {
     assump.push_back(assumption);
   }
-  return checkSatInternal(assump, inUnsatCore, false);
+  return checkSatInternal(assump, false);
 }
 
-Result SmtEngine::checkSat(const std::vector<Node>& assumptions,
-                           bool inUnsatCore)
+Result SmtEngine::checkSat(const std::vector<Node>& assumptions)
 {
   if (Dump.isOn("benchmark"))
   {
@@ -861,10 +860,10 @@ Result SmtEngine::checkSat(const std::vector<Node>& assumptions,
                                                assumptions);
     }
   }
-  return checkSatInternal(assumptions, inUnsatCore, false);
+  return checkSatInternal(assumptions, false);
 }
 
-Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const Node& node)
 {
   if (Dump.isOn("benchmark"))
   {
@@ -872,19 +871,16 @@ Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore)
   }
   return checkSatInternal(
              node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
-             inUnsatCore,
              true)
       .asEntailmentResult();
 }
 
-Result SmtEngine::checkEntailed(const std::vector<Node>& nodes,
-                                bool inUnsatCore)
+Result SmtEngine::checkEntailed(const std::vector<Node>& nodes)
 {
-  return checkSatInternal(nodes, inUnsatCore, true).asEntailmentResult();
+  return checkSatInternal(nodes, true).asEntailmentResult();
 }
 
 Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
-                                   bool inUnsatCore,
                                    bool isEntailmentCheck)
 {
   try
@@ -897,7 +893,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
                  << assumptions << ")" << endl;
     // check the satisfiability with the solver object
     Result r = d_smtSolver->checkSatisfiability(
-        *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck);
+        *d_asserts.get(), assumptions, isEntailmentCheck);
 
     Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
                  << "(" << assumptions << ") => " << r << endl;
@@ -995,7 +991,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
   return res;
 }
 
-Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
+Result SmtEngine::assertFormula(const Node& formula)
 {
   SmtScope smts(this);
   finishInit();
@@ -1011,7 +1007,7 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
   // Substitute out any abstract values in ex
   Node n = d_absValues->substituteAbstractValues(formula);
 
-  d_asserts->assertFormula(n, inUnsatCore);
+  d_asserts->assertFormula(n);
   return quickCheck().asEntailmentResult();
 }/* SmtEngine::assertFormula() */
 

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 357f60b854b7def6e49cfe58e59344984b4b0780..68b1caad026a9642e62290f2fa7d716e33d74801 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -359,13 +359,12 @@ class CVC5_EXPORT SmtEngine
    * Add a formula to the current context: preprocess, do per-theory
    * setup, use processAssertionList(), asserting to T-solver for
    * literals and conjunction of literals.  Returns false if
-   * immediately determined to be inconsistent.  This version
-   * takes a Boolean flag to determine whether to include this asserted
-   * formula in an unsat core (if one is later requested).
+   * immediately determined to be inconsistent. Note this formula will
+   * be included in the unsat core when applicable.
    *
    * @throw TypeCheckingException, LogicException, UnsafeInterruptException
    */
-  Result assertFormula(const Node& formula, bool inUnsatCore = true);
+  Result assertFormula(const Node& formula);
 
   /**
    * Reduce an unsatisfiable core to make it minimal.
@@ -380,9 +379,8 @@ class CVC5_EXPORT SmtEngine
    *
    * @throw Exception
    */
-  Result checkEntailed(const Node& assumption, bool inUnsatCore = true);
-  Result checkEntailed(const std::vector<Node>& assumptions,
-                       bool inUnsatCore = true);
+  Result checkEntailed(const Node& assumption);
+  Result checkEntailed(const std::vector<Node>& assumptions);
 
   /**
    * Assert a formula (if provided) to the current context and call
@@ -391,9 +389,8 @@ class CVC5_EXPORT SmtEngine
    * @throw Exception
    */
   Result checkSat();
-  Result checkSat(const Node& assumption, bool inUnsatCore = true);
-  Result checkSat(const std::vector<Node>& assumptions,
-                  bool inUnsatCore = true);
+  Result checkSat(const Node& assumption);
+  Result checkSat(const std::vector<Node>& assumptions);
 
   /**
    * Returns a set of so-called "failed" assumptions.
@@ -1008,7 +1005,6 @@ class CVC5_EXPORT SmtEngine
    * Check satisfiability (used to check satisfiability and entailment).
    */
   Result checkSatInternal(const std::vector<Node>& assumptions,
-                          bool inUnsatCore,
                           bool isEntailmentCheck);
 
   /**

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index f5783ab6b34f29ec56267b08b50b974924545e2b..6d3326603e77970e425eee649bf53354d7f13485 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -133,7 +133,6 @@ void SmtSolver::shutdown()
 
 Result SmtSolver::checkSatisfiability(Assertions& as,
                                       const std::vector<Node>& assumptions,
-                                      bool inUnsatCore,
                                       bool isEntailmentCheck)
 {
   // update the state to indicate we are about to run a check-sat
@@ -141,7 +140,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
   d_state.notifyCheckSat(hasAssumptions);
 
   // then, initialize the assertions
-  as.initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
+  as.initializeCheckSat(assumptions, isEntailmentCheck);
 
   // make the check
   Assert(d_smt.isFullyInited());

diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 01e52fbfa5adbd3401ca30e1f83161d0d05446c2..ea89f6d575638df22ec3624b6850edcb9edd536b 100644 (file)
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -103,13 +103,11 @@ class SmtSolver
    * during this call.
    * @param assumptions The assumptions for this check-sat call, which are
    * temporary assertions.
-   * @param inUnsatCore Whether assumptions are in the unsat core.
    * @param isEntailmentCheck Whether this is an entailment check (assumptions
    * are negated in this case).
    */
   Result checkSatisfiability(Assertions& as,
                              const std::vector<Node>& assumptions,
-                             bool inUnsatCore,
                              bool isEntailmentCheck);
   /**
    * Process the assertions that have been asserted in as. This moves the set of

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 98278ef9e20e41ea5411930a52765587b28cdd32..d5cfe274eedffae22958de6ff5240f140dd8273d 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -221,7 +221,7 @@ Result SygusSolver::checkSynth(Assertions& as)
     query.push_back(body);
   }
 
-  Result r = d_smtSolver.checkSatisfiability(as, query, false, false);
+  Result r = d_smtSolver.checkSatisfiability(as, query, false);
 
   // Check that synthesis solutions satisfy the conjecture
   if (options::checkSynthSol()