--- /dev/null
+/********************* */
+/*! \file assertions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The module for storing assertions for an SMT engine.
+ **/
+
+#include "smt/assertions.h"
+
+#include "expr/node_algorithm.h"
+#include "options/base_options.h"
+#include "options/language.h"
+#include "options/proof_options.h"
+#include "options/smt_options.h"
+#include "proof/proof_manager.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace smt {
+
+Assertions::Assertions(context::UserContext* u, AbstractValues& absv)
+ : d_userContext(u),
+ d_absValues(absv),
+ d_assertionList(nullptr),
+ d_globalNegation(false),
+ d_assertions()
+{
+}
+
+Assertions::~Assertions()
+{
+ if (d_assertionList != nullptr)
+ {
+ d_assertionList->deleteSelf();
+ }
+}
+
+void Assertions::finishInit()
+{
+ // [MGD 10/20/2011] keep around in incremental mode, due to a
+ // cleanup ordering issue and Nodes/TNodes. If SAT is popped
+ // first, some user-context-dependent TNodes might still exist
+ // with rc == 0.
+ if (options::produceAssertions() || options::incrementalSolving())
+ {
+ // In the case of incremental solving, we appear to need these to
+ // ensure the relevant Nodes remain live.
+ d_assertionList = new (true) AssertionList(d_userContext);
+ d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
+ }
+}
+
+void Assertions::clearCurrent()
+{
+ d_assertions.clear();
+ d_assertions.getIteSkolemMap().clear();
+}
+
+void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
+ bool inUnsatCore,
+ bool isEntailmentCheck)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ // reset global negation
+ d_globalNegation = false;
+ // clear the assumptions
+ d_assumptions.clear();
+ if (isEntailmentCheck)
+ {
+ size_t size = assumptions.size();
+ if (size > 1)
+ {
+ /* Assume: not (BIGAND assumptions) */
+ d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode());
+ }
+ else if (size == 1)
+ {
+ /* Assume: not expr */
+ d_assumptions.push_back(assumptions[0].notNode());
+ }
+ }
+ else
+ {
+ /* Assume: BIGAND assumptions */
+ d_assumptions = assumptions;
+ }
+
+ Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ for (const Node& e : d_assumptions)
+ {
+ // Substitute out any abstract values in ex.
+ Node n = d_absValues.substituteAbstractValues(e);
+ // Ensure expr is type-checked at this point.
+ ensureBoolean(n);
+
+ /* Add assumption */
+ if (d_assertionList != nullptr)
+ {
+ d_assertionList->push_back(n);
+ }
+ addFormula(n, inUnsatCore, true, true, false);
+ }
+ if (d_globalDefineFunRecLemmas != nullptr)
+ {
+ // Global definitions are asserted at check-sat-time because we have to
+ // make sure that they are always present (they are essentially level
+ // zero assertions)
+ for (const Node& lemma : *d_globalDefineFunRecLemmas)
+ {
+ addFormula(lemma, false, true, false, false);
+ }
+ }
+}
+
+void Assertions::assertFormula(const Node& n, bool inUnsatCore)
+{
+ ensureBoolean(n);
+ if (d_assertionList != nullptr)
+ {
+ d_assertionList->push_back(n);
+ }
+ bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+ addFormula(n, inUnsatCore, true, false, maybeHasFv);
+}
+
+std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
+bool Assertions::isGlobalNegated() const { return d_globalNegation; }
+void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; }
+
+preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
+{
+ return d_assertions;
+}
+
+context::CDList<Node>* Assertions::getAssertionList()
+{
+ return d_assertionList;
+}
+
+void Assertions::addFormula(
+ TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
+{
+ if (n.isConst() && n.getConst<bool>())
+ {
+ // true, nothing to do
+ return;
+ }
+
+ Trace("smt") << "SmtEnginePrivate::addFormula(" << n
+ << "), inUnsatCore = " << inUnsatCore
+ << ", inInput = " << inInput
+ << ", isAssumption = " << isAssumption << std::endl;
+
+ // Ensure that it does not contain free variables
+ if (maybeHasFv)
+ {
+ if (expr::hasFreeVar(n))
+ {
+ std::stringstream se;
+ se << "Cannot process assertion with free variable.";
+ if (language::isInputLangSygus(options::inputLanguage()))
+ {
+ // Common misuse of SyGuS is to use top-level assert instead of
+ // constraint when defining the synthesis conjecture.
+ se << " Perhaps you meant `constraint` instead of `assert`?";
+ }
+ throw ModalException(se.str().c_str());
+ }
+ }
+
+ // Give it to proof manager
+ PROOF(if (inInput) {
+ // n is an input assertion
+ if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores()
+ || options::checkUnsatCores() || options::fewerPreprocessingHoles())
+ {
+ ProofManager::currentPM()->addCoreAssertion(n.toExpr());
+ }
+ } else {
+ // n is the result of an unknown preprocessing step, add it to dependency
+ // map to null
+ ProofManager::currentPM()->addDependence(n, Node::null());
+ });
+
+ // Add the normalized formula to the queue
+ d_assertions.push_back(n, isAssumption);
+}
+
+void Assertions::addDefineFunRecDefinition(Node n, bool global)
+{
+ n = d_absValues.substituteAbstractValues(n);
+ if (d_assertionList != nullptr)
+ {
+ d_assertionList->push_back(n);
+ }
+ if (global && d_globalDefineFunRecLemmas != nullptr)
+ {
+ // Global definitions are asserted at check-sat-time because we have to
+ // make sure that they are always present
+ Assert(!language::isInputLangSygus(options::inputLanguage()));
+ d_globalDefineFunRecLemmas->emplace_back(n);
+ }
+ else
+ {
+ bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+ addFormula(n, false, true, false, maybeHasFv);
+ }
+}
+
+void Assertions::ensureBoolean(const Node& n)
+{
+ TypeNode type = n.getType(options::typeChecking());
+ if (!type.isBoolean())
+ {
+ std::stringstream ss;
+ ss << "Expected Boolean type\n"
+ << "The assertion : " << n << "\n"
+ << "Its type : " << type;
+ throw TypeCheckingException(n.toExpr(), ss.str());
+ }
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file assertions.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The module for storing assertions for an SMT engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__ASSERTIONS_H
+#define CVC4__SMT__ASSERTIONS_H
+
+#include <vector>
+
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "smt/abstract_values.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * Contains all information pertaining to the assertions of an SMT engine.
+ *
+ * This class is responsible for setting up the assertions pipeline for
+ * check-sat calls. It is *not* responsible for the preprocessing itself, and
+ * instead is intended to be the input to a preprocessor utility.
+ */
+class Assertions
+{
+ /** The type of our internal assertion list */
+ typedef context::CDList<Node> AssertionList;
+
+ public:
+ Assertions(context::UserContext* u, AbstractValues& absv);
+ ~Assertions();
+ /**
+ * Finish initialization, called once after options are finalized. Sets up
+ * the required bookkeeping based on the options.
+ */
+ void finishInit();
+ /**
+ * Clears out the non-context-dependent data in this class. Necessary to
+ * clear out our assertion vectors in case someone does a push-assert-pop
+ * without a check-sat.
+ */
+ void clearCurrent();
+ /*
+ * Initialize a call to check satisfiability. This adds assumptions to
+ * the list of assumptions maintained by this class, and finalizes the
+ * set of formulas (in the assertions pipeline) that will be used for the
+ * 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).
+ *
+ * @throw TypeCheckingException, LogicException, UnsafeInterruptException
+ */
+ void assertFormula(const Node& n, bool inUnsatCore = true);
+ /**
+ * Assert that n corresponds to an assertion from a define-fun-rec command.
+ * This assertion is added to the set of assertions maintained by this class.
+ * If this has a global definition, this assertion is persistent for any
+ * subsequent check-sat calls.
+ */
+ void addDefineFunRecDefinition(Node n, bool global);
+ /**
+ * Get the assertions pipeline, which contains the set of assertions we are
+ * currently processing.
+ */
+ preprocessing::AssertionPipeline& getAssertionPipeline();
+ /**
+ * Get assertions list corresponding to the original list of assertions,
+ * before preprocessing.
+ */
+ context::CDList<Node>* getAssertionList();
+ /**
+ * Get the list of assumptions, which are those registered to this class
+ * on initializeCheckSat.
+ */
+ std::vector<Node>& getAssumptions();
+ /**
+ * Is the set of assertions globally negated? When this flag is true, the
+ * overall result of check-sat should be inverted.
+ */
+ bool isGlobalNegated() const;
+ /** Flip the global negation flag. */
+ void flipGlobalNegated();
+
+ private:
+ /**
+ * Fully type-check the argument, and also type-check that it's
+ * actually Boolean.
+ * throw@ TypeCheckingException
+ */
+ void ensureBoolean(const Node& n);
+ /**
+ * Adds a formula to the current context. Action here depends on
+ * the SimplificationMode (in the current Options scope); the
+ * formula might be pushed out to the propositional layer
+ * immediately, or it might be simplified and kept, or it might not
+ * even be simplified.
+ * The arguments isInput and isAssumption are used for bookkeeping for proofs.
+ * The argument maybeHasFv should be set to true if the assertion may have
+ * free variables. By construction, assertions from the smt2 parser are
+ * guaranteed not to have free variables. However, other cases such as
+ * assertions from the SyGuS parser may have free variables (say if the
+ * input contains an assert or define-fun-rec command).
+ *
+ * @param isAssumption If true, the formula is considered to be an assumption
+ * (this is used to distinguish assertions and assumptions)
+ */
+ void addFormula(TNode n,
+ bool inUnsatCore,
+ bool inInput,
+ bool isAssumption,
+ bool maybeHasFv);
+ /** pointer to the user context */
+ context::UserContext* d_userContext;
+ /** Reference to the abstract values utility */
+ AbstractValues& d_absValues;
+ /**
+ * The assertion list (before any conversion) for supporting
+ * getAssertions(). Only maintained if in incremental mode.
+ */
+ AssertionList* d_assertionList;
+ /**
+ * List of lemmas generated for global recursive function definitions. We
+ * assert this list of definitions in each check-sat call.
+ */
+ std::unique_ptr<std::vector<Node>> d_globalDefineFunRecLemmas;
+ /**
+ * The list of assumptions from the previous call to checkSatisfiability.
+ * Note that if the last call to checkSatisfiability was an entailment check,
+ * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains
+ * one single assumption ~(a1 AND ... AND an).
+ */
+ std::vector<Node> d_assumptions;
+ /** Whether we did a global negation of the formula. */
+ bool d_globalNegation;
+ /** Assertions in the preprocessing pipeline */
+ preprocessing::AssertionPipeline d_assertions;
+};
+
+} // namespace smt
+} // namespace CVC4
+
+#endif
#include "prop/prop_engine.h"
#include "smt/abduction_solver.h"
#include "smt/abstract_values.h"
+#include "smt/assertions.h"
#include "smt/expr_names.h"
#include "smt/command.h"
#include "smt/defined_function.h"
/** A circuit propagator for non-clausal propositional deduction */
booleans::CircuitPropagator d_propagator;
- /** Assertions in the preprocessing pipeline */
- AssertionPipeline d_assertions;
-
/** Whether any assertions have been processed */
CDO<bool> d_assertionsProcessed;
ProcessAssertions d_processor;
public:
- IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); }
/** Instance of the ITE remover */
RemoveTermFormulas d_iteRemover;
SmtEnginePrivate(SmtEngine& smt)
: d_smt(smt),
d_propagator(true, true),
- d_assertions(),
d_assertionsProcessed(smt.getUserContext(), false),
d_processor(smt, *smt.getResourceManager()),
d_iteRemover(smt.getUserContext()),
/**
* Process the assertions that have been asserted.
*/
- void processAssertions();
+ void processAssertions(Assertions& as);
/** Process a user push.
*/
void notifyPush() {
-
}
/**
* last map of expression names from notifyPush.
*/
void notifyPop() {
- d_assertions.clear();
d_propagator.getLearnedLiterals().clear();
- getIteSkolemMap().clear();
}
-
- /**
- * Adds a formula to the current context. Action here depends on
- * the SimplificationMode (in the current Options scope); the
- * formula might be pushed out to the propositional layer
- * immediately, or it might be simplified and kept, or it might not
- * even be simplified.
- * The arguments isInput and isAssumption are used for bookkeeping for proofs.
- * The argument maybeHasFv should be set to true if the assertion may have
- * free variables. By construction, assertions from the smt2 parser are
- * guaranteed not to have free variables. However, other cases such as
- * assertions from the SyGuS parser may have free variables (say if the
- * input contains an assert or define-fun-rec command).
- *
- * @param isAssumption If true, the formula is considered to be an assumption
- * (this is used to distinguish assertions and assumptions)
- */
- void addFormula(TNode n,
- bool inUnsatCore,
- bool inInput = true,
- bool isAssumption = false,
- bool maybeHasFv = false);
/**
* Simplify node "in" by expanding definitions and applying any
* substitutions learned from preprocessing.
// Expand definitions.
NodeToNodeHashMap cache;
Node n = d_processor.expandDefinitions(in, cache).toExpr();
- // Make sure we've done all preprocessing, etc.
- Assert(d_assertions.size() == 0);
return applySubstitutions(n).toExpr();
}
};/* class SmtEnginePrivate */
d_exprManager(em),
d_nodeManager(d_exprManager->getNodeManager()),
d_absValues(new AbstractValues(d_nodeManager)),
+ d_asserts(new Assertions(d_userContext.get(), *d_absValues.get())),
d_exprNames(new ExprNames(d_userContext.get())),
d_dumpm(new DumpManager(d_userContext.get())),
d_routListener(new ResourceOutListener(*this)),
d_rewriter(new theory::Rewriter()),
d_definedFunctions(nullptr),
d_abductSolver(nullptr),
- d_assertionList(nullptr),
d_assignments(nullptr),
d_defineCommands(),
d_logic(),
d_fullyInited(false),
d_queryMade(false),
d_needPostsolve(false),
- d_globalNegation(false),
d_status(),
d_expectedStatus(),
d_smtMode(SMT_MODE_START),
d_userContext->push();
d_context->push();
- Trace("smt-debug") << "Set up assertion list..." << std::endl;
- // [MGD 10/20/2011] keep around in incremental mode, due to a
- // cleanup ordering issue and Nodes/TNodes. If SAT is popped
- // first, some user-context-dependent TNodes might still exist
- // with rc == 0.
- if(options::produceAssertions() ||
- options::incrementalSolving()) {
- // In the case of incremental solving, we appear to need these to
- // ensure the relevant Nodes remain live.
- d_assertionList = new (true) AssertionList(getUserContext());
- d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
- }
+ Trace("smt-debug") << "Set up assertions..." << std::endl;
+ d_asserts->finishInit();
// dump out a set-logic command only when raw-benchmark is disabled to avoid
// dumping the command twice.
d_assignments->deleteSelf();
}
- d_globalDefineFunRecLemmas.reset();
-
- if(d_assertionList != NULL) {
- d_assertionList->deleteSelf();
- }
-
d_definedFunctions->deleteSelf();
//destroy all passes before destroying things that they refer to
#endif
d_absValues.reset(nullptr);
+ d_asserts.reset(nullptr);
d_exprNames.reset(nullptr);
d_dumpm.reset(nullptr);
d_userLogic.lock();
}
-void SmtEngine::setProblemExtended()
-{
- d_smtMode = SMT_MODE_ASSERT;
- d_assumptions.clear();
-}
-
void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
{
SmtScope smts(this);
}
ExprManager* em = getExprManager();
- bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
for (unsigned i = 0, size = funcs.size(); i < size; i++)
{
// we assert a quantified formula
// assert the quantified formula
// notice we don't call assertFormula directly, since this would
// duplicate the output on raw-benchmark.
- Node n = d_absValues->substituteAbstractValues(Node::fromExpr(lem));
- if (d_assertionList != nullptr)
- {
- d_assertionList->push_back(n);
- }
- if (global && d_globalDefineFunRecLemmas != nullptr)
- {
- // Global definitions are asserted at check-sat-time because we have to
- // make sure that they are always present
- Assert(!language::isInputLangSygus(options::inputLanguage()));
- d_globalDefineFunRecLemmas->emplace_back(n);
- }
- else
- {
- d_private->addFormula(n, false, true, false, maybeHasFv);
- }
+ Node lemn = Node::fromExpr(lem);
+ // add define recursive definition to the assertions
+ d_asserts->addDefineFunRecDefinition(lemn, global);
}
}
// Make sure the prop layer has all of the assertions
Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
- d_private->processAssertions();
+ d_private->processAssertions(*d_asserts);
Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
return m;
}
-void SmtEnginePrivate::processAssertions() {
+void SmtEnginePrivate::processAssertions(Assertions& as)
+{
TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
spendResource(ResourceManager::Resource::PreprocessStep);
Assert(d_smt.d_fullyInited);
Assert(d_smt.d_pendingPops == 0);
- if (d_assertions.size() == 0) {
+ AssertionPipeline& ap = as.getAssertionPipeline();
+
+ if (ap.size() == 0)
+ {
// nothing to do
return;
}
// TODO(b/1255): Substitutions in incremental mode should be managed with a
// proper data structure.
- d_assertions.enableStoreSubstsInAsserts();
+ ap.enableStoreSubstsInAsserts();
}
else
{
- d_assertions.disableStoreSubstsInAsserts();
+ ap.disableStoreSubstsInAsserts();
}
// process the assertions
- bool noConflict = d_processor.apply(d_assertions);
+ bool noConflict = d_processor.apply(as);
//notify theory engine new preprocessed assertions
- d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() );
+ d_smt.d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
// Push the formula to decision engine
if (noConflict)
{
Chat() << "pushing to decision engine..." << endl;
- d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions);
+ d_smt.d_propEngine->addAssertionsToDecisionEngine(ap);
}
// end: INVARIANT to maintain: no reordering of assertions or
// if incremental, compute which variables are assigned
if (options::incrementalSolving())
{
- d_preprocessingPassContext->recordSymbolsInAssertions(d_assertions.ref());
+ d_preprocessingPassContext->recordSymbolsInAssertions(ap.ref());
}
// Push the formula to SAT
{
Chat() << "converting to CNF..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- Chat() << "+ " << d_assertions[i] << std::endl;
- d_smt.d_propEngine->assertFormula(d_assertions[i]);
- }
- }
-
- d_assertionsProcessed = true;
-
- d_assertions.clear();
- getIteSkolemMap().clear();
-}
-
-void SmtEnginePrivate::addFormula(
- TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
-{
- if (n == d_true) {
- // nothing to do
- return;
- }
-
- Trace("smt") << "SmtEnginePrivate::addFormula(" << n
- << "), inUnsatCore = " << inUnsatCore
- << ", inInput = " << inInput
- << ", isAssumption = " << isAssumption << endl;
-
- // Ensure that it does not contain free variables
- if (maybeHasFv)
- {
- if (expr::hasFreeVar(n))
+ for (const Node& assertion : ap.ref())
{
- std::stringstream se;
- se << "Cannot process assertion with free variable.";
- if (language::isInputLangSygus(options::inputLanguage()))
- {
- // Common misuse of SyGuS is to use top-level assert instead of
- // constraint when defining the synthesis conjecture.
- se << " Perhaps you meant `constraint` instead of `assert`?";
- }
- throw ModalException(se.str().c_str());
+ Chat() << "+ " << assertion << std::endl;
+ d_smt.d_propEngine->assertFormula(assertion);
}
}
- // Give it to proof manager
- PROOF(
- if( inInput ){
- // n is an input assertion
- if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
-
- ProofManager::currentPM()->addCoreAssertion(n.toExpr());
- }
- }else{
- // n is the result of an unknown preprocessing step, add it to dependency map to null
- ProofManager::currentPM()->addDependence(n, Node::null());
- }
- );
-
- // Add the normalized formula to the queue
- d_assertions.push_back(n, isAssumption);
- //d_assertions.push_back(Rewriter::rewrite(n));
-}
+ d_assertionsProcessed = true;
-void SmtEngine::ensureBoolean(const Node& n)
-{
- TypeNode type = n.getType(options::typeChecking());
- TypeNode boolType = NodeManager::currentNM()->booleanType();
- if(type != boolType) {
- stringstream ss;
- ss << "Expected " << boolType << "\n"
- << "The assertion : " << n << "\n"
- << "Its type : " << type;
- throw TypeCheckingException(n.toExpr(), ss.str());
- }
+ // clear the current assertions
+ as.clearCurrent();
}
Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
{
Dump("benchmark") << CheckSatCommand(assumption);
- return checkSatisfiability(assumption, inUnsatCore, false);
+ return checkSatisfiability(Node::fromExpr(assumption), inUnsatCore, false);
}
Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
{
Dump("benchmark") << CheckSatAssumingCommand(assumptions);
}
-
- return checkSatisfiability(assumptions, inUnsatCore, false);
+ std::vector<Node> assumps;
+ for (const Expr& e : assumptions)
+ {
+ assumps.push_back(Node::fromExpr(e));
+ }
+ return checkSatisfiability(assumps, inUnsatCore, false);
}
-Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore)
{
- Dump("benchmark") << QueryCommand(expr, inUnsatCore);
- return checkSatisfiability(
- expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
- inUnsatCore,
- true)
+ Dump("benchmark") << QueryCommand(node, inUnsatCore);
+ return checkSatisfiability(node.isNull()
+ ? std::vector<Node>()
+ : std::vector<Node>{Node::fromExpr(node)},
+ inUnsatCore,
+ true)
.asEntailmentResult();
}
-Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const vector<Expr>& nodes, bool inUnsatCore)
{
- return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult();
+ std::vector<Node> ns;
+ for (const Expr& e : nodes)
+ {
+ ns.push_back(Node::fromExpr(e));
+ }
+ return checkSatisfiability(ns, inUnsatCore, true).asEntailmentResult();
}
-Result SmtEngine::checkSatisfiability(const Expr& expr,
+Result SmtEngine::checkSatisfiability(const Node& node,
bool inUnsatCore,
bool isEntailmentCheck)
{
return checkSatisfiability(
- expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
+ node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
inUnsatCore,
isEntailmentCheck);
}
-Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
+Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions,
bool inUnsatCore,
bool isEntailmentCheck)
{
"(try --incremental)");
}
- // Note that a query has been made
+ // Note that a query has been made and we are in assert mode
d_queryMade = true;
- // reset global negation
- d_globalNegation = false;
+ d_smtMode = SMT_MODE_ASSERT;
+ // push if there are assumptions
bool didInternalPush = false;
-
- setProblemExtended();
-
- if (isEntailmentCheck)
- {
- size_t size = assumptions.size();
- if (size > 1)
- {
- /* Assume: not (BIGAND assumptions) */
- d_assumptions.push_back(
- d_exprManager->mkExpr(kind::AND, assumptions).notExpr());
- }
- else if (size == 1)
- {
- /* Assume: not expr */
- d_assumptions.push_back(assumptions[0].notExpr());
- }
- }
- else
- {
- /* Assume: BIGAND assumptions */
- d_assumptions = assumptions;
- }
-
- if (!d_assumptions.empty())
+ if (!assumptions.empty())
{
internalPush();
didInternalPush = true;
}
- Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
- for (Expr e : d_assumptions)
- {
- // Substitute out any abstract values in ex.
- Node n = d_absValues->substituteAbstractValues(Node::fromExpr(e));
- // Ensure expr is type-checked at this point.
- ensureBoolean(n);
+ // then, initialize the assertions
+ d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
- /* Add assumption */
- if (d_assertionList != NULL)
- {
- d_assertionList->push_back(n);
- }
- d_private->addFormula(n, inUnsatCore, true, true);
- }
-
- if (d_globalDefineFunRecLemmas != nullptr)
- {
- // Global definitions are asserted at check-sat-time because we have to
- // make sure that they are always present (they are essentially level
- // zero assertions)
- for (const Node& lemma : *d_globalDefineFunRecLemmas)
- {
- d_private->addFormula(lemma, false, true, false, false);
- }
- }
-
- r = check();
+ // make the check
+ Result r = check();
if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
&& r.asSatisfiabilityResult().isSat() == Result::UNSAT)
r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
}
// flipped if we did a global negation
- if (d_globalNegation)
+ if (d_asserts->isGlobalNegated())
{
Trace("smt") << "SmtEngine::process global negate " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
}
}
-vector<Expr> SmtEngine::getUnsatAssumptions(void)
+std::vector<Node> SmtEngine::getUnsatAssumptions(void)
{
Trace("smt") << "SMT getUnsatAssumptions()" << endl;
SmtScope smts(this);
Dump("benchmark") << GetUnsatAssumptionsCommand();
}
UnsatCore core = getUnsatCoreInternal();
- vector<Expr> res;
- for (const Expr& e : d_assumptions)
+ std::vector<Node> res;
+ std::vector<Node>& assumps = d_asserts->getAssumptions();
+ for (const Node& e : assumps)
{
- if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); }
+ if (std::find(core.begin(), core.end(), e.toExpr()) != core.end())
+ {
+ res.push_back(e);
+ }
}
return res;
}
// Substitute out any abstract values in ex
Node n = d_absValues->substituteAbstractValues(formula);
- ensureBoolean(n);
- if(d_assertionList != NULL) {
- d_assertionList->push_back(n);
- }
- bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
- d_private->addFormula(n, inUnsatCore, true, false, maybeHasFv);
+ d_asserts->assertFormula(n, inUnsatCore);
return quickCheck().asEntailmentResult();
}/* SmtEngine::assertFormula() */
}
// Make sure all preprocessing is done
- d_private->processAssertions();
+ d_private->processAssertions(*d_asserts);
Node n = d_private->simplify(Node::fromExpr(e));
n = postprocess(n, TypeNode::fromType(e.getType()));
return n.toExpr();
}
void SmtEngine::checkModel(bool hardFailure) {
+ context::CDList<Node>* al = d_asserts->getAssertionList();
// --check-model implies --produce-assertions, which enables the
// assertion list, so we should be ok.
- Assert(d_assertionList != NULL)
+ Assert(al != nullptr)
<< "don't have an assertion list to check in SmtEngine::checkModel()";
TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
}
// Now go through all our user assertions checking if they're satisfied.
- for (const Node& assertion : *d_assertionList)
+ for (const Node& assertion : *al)
{
Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
<< endl;
Trace("check-synth-sol") << "Retrieving assertions\n";
// Build conjecture from original assertions
- if (d_assertionList == NULL)
+ context::CDList<Node>* al = d_asserts->getAssertionList();
+ if (al == nullptr)
{
Trace("check-synth-sol") << "No assertions to check\n";
return;
std::vector<Node> auxAssertions;
// expand definitions cache
std::unordered_map<Node, Node, NodeHashFunction> cache;
- for (const Node& assertion : *d_assertionList)
+ for (const Node& assertion : *al)
{
Notice() << "SmtEngine::checkSynthSolution(): checking assertion "
<< assertion << endl;
"Cannot query the current assertion list when not in produce-assertions mode.";
throw ModalException(msg);
}
- Assert(d_assertionList != NULL);
+ context::CDList<Node>* al = d_asserts->getAssertionList();
+ Assert(al != nullptr);
std::vector<Expr> res;
- for (const Node& n : *d_assertionList)
+ for (const Node& n : *al)
{
res.emplace_back(n.toExpr());
}
doPendingPops();
Trace("smt") << "SMT push()" << endl;
d_private->notifyPush();
- d_private->processAssertions();
+ d_private->processAssertions(*d_asserts);
if(Dump.isOn("benchmark")) {
Dump("benchmark") << PushCommand();
}
// The problem isn't really "extended" yet, but this disallows
// get-model after a push, simplifying our lives somewhat and
// staying symmetric with pop.
- setProblemExtended();
+ d_smtMode = SMT_MODE_ASSERT;
d_userLevels.push_back(d_userContext->getLevel());
internalPush();
// but also it would be weird to have a legally-executed (get-model)
// that only returns a subset of the assignment (because the rest
// is no longer in scope!).
- setProblemExtended();
+ d_smtMode = SMT_MODE_ASSERT;
AlwaysAssert(d_userContext->getLevel() > 0);
AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
d_userLevels.pop_back();
// Clear out assertion queues etc., in case anything is still in there
+ d_asserts->clearCurrent();
d_private->notifyPop();
Trace("userpushpop") << "SmtEngine: popped to level "
Trace("smt") << "SmtEngine::internalPush()" << endl;
doPendingPops();
if(options::incrementalSolving()) {
- d_private->processAssertions();
+ d_private->processAssertions(*d_asserts);
TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
d_userContext->push();
// the d_context push is done inside of the SAT solver
projects / cvc5.git / commitdiff