#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
#include "proof/unsat_core.h"
-#include "prop/prop_engine.h"
#include "smt/abduction_solver.h"
#include "smt/abstract_values.h"
#include "smt/assertions.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_engine_state.h"
#include "smt/smt_engine_stats.h"
+#include "smt/smt_solver.h"
#include "smt/term_formula_removal.h"
#include "smt/update_ostream.h"
#include "smt_util/boolean_simplification.h"
d_dumpm(new DumpManager(getUserContext())),
d_routListener(new ResourceOutListener(*this)),
d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
- d_theoryEngine(nullptr),
- d_propEngine(nullptr),
+ d_smtSolver(nullptr),
d_proofManager(nullptr),
d_rewriter(new theory::Rewriter()),
d_definedFunctions(nullptr),
d_resourceManager->registerListener(d_routListener.get());
// make statistics
d_stats.reset(new SmtEngineStatistics());
-
+ // make the SMT solver
+ d_smtSolver.reset(
+ new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats));
+
// The ProofManager is constructed before any other proof objects such as
// SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
// initialized in TheoryEngine and PropEngine respectively.
}
context::Context* SmtEngine::getContext() { return d_state->getContext(); }
+TheoryEngine* SmtEngine::getTheoryEngine()
+{
+ return d_smtSolver->getTheoryEngine();
+}
+
+prop::PropEngine* SmtEngine::getPropEngine()
+{
+ return d_smtSolver->getPropEngine();
+}
+
void SmtEngine::finishInit()
{
if (d_state->isFullyInited())
d_optm->finishInit(d_logic, d_isInternalSubsolver);
Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
- // We have mutual dependency here, so we add the prop engine to the theory
- // engine later (it is non-essential there)
- d_theoryEngine.reset(new TheoryEngine(getContext(),
- getUserContext(),
- getResourceManager(),
- d_pp->getTermFormulaRemover(),
- const_cast<const LogicInfo&>(d_logic)));
-
- // Add the theories
- for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
- TheoryConstructor::addTheory(getTheoryEngine(), id);
- //register with proof engine if applicable
-#ifdef CVC4_PROOF
- ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id));
-#endif
- }
-
- Trace("smt-debug") << "Making decision engine..." << std::endl;
-
- Trace("smt-debug") << "Making prop engine..." << std::endl;
- /* force destruction of referenced PropEngine to enforce that statistics
- * are unregistered by the obsolete PropEngine object before registered
- * again by the new PropEngine object */
- d_propEngine.reset(nullptr);
- d_propEngine.reset(new PropEngine(
- getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
-
- Trace("smt-debug") << "Setting up theory engine..." << std::endl;
- d_theoryEngine->setPropEngine(getPropEngine());
- Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
- d_theoryEngine->finishInit();
+ d_smtSolver->finishInit(const_cast<const LogicInfo&>(d_logic));
// global push/pop around everything, to ensure proper destruction
// of context-dependent data structures
PROOF( ProofManager::currentPM()->setLogic(d_logic); );
PROOF({
- for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
- ProofManager::currentPM()->getTheoryProofEngine()->
- finishRegisterTheory(d_theoryEngine->theoryOf(id));
- }
- });
+ TheoryEngine* te = d_smtSolver->getTheoryEngine();
+ for (TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id)
+ {
+ ProofManager::currentPM()->getTheoryProofEngine()->finishRegisterTheory(
+ te->theoryOf(id));
+ }
+ });
d_pp->finishInit();
- AlwaysAssert(d_propEngine->getAssertionLevel() == 0)
+ AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
<< "The PropEngine has pushed but the SmtEngine "
"hasn't finished initializing!";
void SmtEngine::shutdown() {
d_state->shutdown();
- if (d_propEngine != nullptr)
- {
- d_propEngine->shutdown();
- }
- if (d_theoryEngine != nullptr)
- {
- d_theoryEngine->shutdown();
- }
+ d_smtSolver->shutdown();
}
SmtEngine::~SmtEngine()
d_exprNames.reset(nullptr);
d_dumpm.reset(nullptr);
- d_theoryEngine.reset(nullptr);
- d_propEngine.reset(nullptr);
+ d_smtSolver.reset(nullptr);
d_stats.reset(nullptr);
d_private.reset(nullptr);
return d_definedFunctions->find(nf) != d_definedFunctions->end();
}
-Result SmtEngine::check() {
- Assert(d_state->isFullyReady());
-
- Trace("smt") << "SmtEngine::check()" << endl;
-
- const std::string& filename = d_state->getFilename();
- if (d_resourceManager->out())
- {
- Result::UnknownExplanation why = d_resourceManager->outOfResources()
- ? Result::RESOURCEOUT
- : Result::TIMEOUT;
- return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
- }
- d_resourceManager->beginCall();
-
- // Make sure the prop layer has all of the assertions
- Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
- processAssertionsInternal();
- Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
-
- TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
-
- Chat() << "solving..." << endl;
- Trace("smt") << "SmtEngine::check(): running check" << endl;
- Result result = d_propEngine->checkSat();
-
- d_resourceManager->endCall();
- Trace("limit") << "SmtEngine::check(): cumulative millis "
- << d_resourceManager->getTimeUsage() << ", resources "
- << d_resourceManager->getResourceUsage() << endl;
-
- return Result(result, filename);
-}
-
Result SmtEngine::quickCheck() {
Assert(d_state->isFullyInited());
Trace("smt") << "SMT quickCheck()" << endl;
throw ModalException(ss.str().c_str());
}
- TheoryModel* m = d_theoryEngine->getBuiltModel();
+ TheoryEngine* te = d_smtSolver->getTheoryEngine();
+ Assert(te != nullptr);
+ TheoryModel* m = te->getBuiltModel();
if (m == nullptr)
{
return m;
}
-void SmtEngine::notifyPushPre() { processAssertionsInternal(); }
+void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); }
+
void SmtEngine::notifyPushPost()
{
TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
- d_propEngine->push();
+ Assert(getPropEngine() != nullptr);
+ getPropEngine()->push();
}
+
void SmtEngine::notifyPopPre()
{
TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
- d_propEngine->pop();
+ PropEngine* pe = getPropEngine();
+ Assert(pe != nullptr);
+ pe->pop();
}
-void SmtEngine::notifyPostSolvePre() { d_propEngine->resetTrail(); }
-void SmtEngine::notifyPostSolvePost() { d_theoryEngine->postsolve(); }
-void SmtEngine::processAssertionsInternal()
+void SmtEngine::notifyPostSolvePre()
{
- TimerStat::CodeTimer paTimer(d_stats->d_processAssertionsTime);
- d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
- Assert(d_state->isFullyReady());
-
- AssertionPipeline& ap = d_asserts->getAssertionPipeline();
-
- if (ap.size() == 0)
- {
- // nothing to do
- return;
- }
-
- // process the assertions with the preprocessor
- bool noConflict = d_pp->process(*d_asserts);
-
- //notify theory engine new preprocessed assertions
- d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
-
- // Push the formula to decision engine
- if (noConflict)
- {
- Chat() << "pushing to decision engine..." << endl;
- d_propEngine->addAssertionsToDecisionEngine(ap);
- }
-
- // end: INVARIANT to maintain: no reordering of assertions or
- // introducing new ones
-
- d_pp->postprocess(*d_asserts);
-
- // Push the formula to SAT
- {
- Chat() << "converting to CNF..." << endl;
- TimerStat::CodeTimer codeTimer(d_stats->d_cnfConversionTime);
- for (const Node& assertion : ap.ref())
- {
- Chat() << "+ " << assertion << std::endl;
- d_propEngine->assertFormula(assertion);
- }
- }
+ PropEngine* pe = getPropEngine();
+ Assert(pe != nullptr);
+ pe->resetTrail();
+}
- // clear the current assertions
- d_asserts->clearCurrent();
+void SmtEngine::notifyPostSolvePost()
+{
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ te->postsolve();
}
Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
{
Dump("benchmark") << CheckSatCommand(assumption);
- return checkSatisfiability(Node::fromExpr(assumption), inUnsatCore, false);
+ std::vector<Node> assump;
+ if (!assumption.isNull())
+ {
+ assump.push_back(Node::fromExpr(assumption));
+ }
+ return checkSatInternal(assump, inUnsatCore, false);
}
Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
{
assumps.push_back(Node::fromExpr(e));
}
- return checkSatisfiability(assumps, inUnsatCore, false);
+ return checkSatInternal(assumps, inUnsatCore, false);
}
Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore)
{
Dump("benchmark") << QueryCommand(node, inUnsatCore);
- return checkSatisfiability(node.isNull()
- ? std::vector<Node>()
- : std::vector<Node>{Node::fromExpr(node)},
- inUnsatCore,
- true)
+ return checkSatInternal(node.isNull()
+ ? std::vector<Node>()
+ : std::vector<Node>{Node::fromExpr(node)},
+ inUnsatCore,
+ true)
.asEntailmentResult();
}
{
ns.push_back(Node::fromExpr(e));
}
- return checkSatisfiability(ns, inUnsatCore, true).asEntailmentResult();
+ return checkSatInternal(ns, inUnsatCore, true).asEntailmentResult();
}
-Result SmtEngine::checkSatisfiability(const Node& node,
- bool inUnsatCore,
- bool isEntailmentCheck)
-{
- return checkSatisfiability(
- node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
- inUnsatCore,
- isEntailmentCheck);
-}
-
-Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions,
- bool inUnsatCore,
- bool isEntailmentCheck)
+Result SmtEngine::checkSatInternal(const vector<Node>& assumptions,
+ bool inUnsatCore,
+ bool isEntailmentCheck)
{
try
{
Trace("smt") << "SmtEngine::"
<< (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
<< assumptions << ")" << endl;
- // update the state to indicate we are about to run a check-sat
- bool hasAssumptions = !assumptions.empty();
- d_state->notifyCheckSat(hasAssumptions);
-
- // then, initialize the assertions
- d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
-
- // 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_asserts->isGlobalNegated())
- {
- Trace("smt") << "SmtEngine::process global negate " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
- {
- r = Result(Result::SAT);
- }
- else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
- {
- // only if satisfaction complete
- if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
- {
- r = Result(Result::UNSAT);
- }
- else
- {
- r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
- }
- }
- Trace("smt") << "SmtEngine::global negate returned " << r << std::endl;
- }
-
- // notify our state of the check-sat result
- d_state->notifyCheckSatResult(hasAssumptions, r);
+ // check the satisfiability with the solver object
+ Result r = d_smtSolver->checkSatisfiability(
+ *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck);
Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
<< "(" << assumptions << ") => " << r << endl;
throw ModalException(
"Cannot make check-synth commands when incremental solving is enabled");
}
- Expr query;
+ std::vector<Node> query;
if (d_private->d_sygusConjectureStale)
{
// build synthesis conjecture from asserted constraints and declared
d_private->d_sygusConjectureStale = false;
// TODO (project #7): if incremental, we should push a context and assert
- query = body.toExpr();
+ query.push_back(body);
}
- Result r = checkSatisfiability(query, true, false);
+ Result r = checkSatInternal(query, true, false);
// Check that synthesis solutions satisfy the conjecture
if (options::checkSynthSol()
finishInit();
d_state->doPendingPops();
// ensure we've processed assertions
- processAssertionsInternal();
+ d_smtSolver->processAssertions(*d_asserts);
return d_pp->simplify(ex);
}
// Since model m is being returned to the user, we must ensure that this
// model object remains valid with future check-sat calls. Hence, we set
// the theory engine into "eager model building" mode. TODO #2648: revisit.
- d_theoryEngine->setEagerModelBuilding();
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ te->setEagerModelBuilding();
if (options::modelCoresMode() != options::ModelCoresMode::NONE)
{
// Check individual theory assertions
if (options::debugCheckModels())
{
- d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure);
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ te->checkTheoryAssertionsWithModel(hardFailure);
}
// Output the model
NodeManager* nm = NodeManager::currentNM();
Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl;
std::map<Node, std::map<Node, Node>> sol_map;
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
/* Get solutions and build auxiliary vectors for substituting */
- if (!d_theoryEngine->getSynthSolutions(sol_map))
+ if (!te->getSynthSolutions(sol_map))
{
InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!";
return;
out << "% SZS output start Proof for " << d_state->getFilename()
<< std::endl;
}
- if( d_theoryEngine ){
- d_theoryEngine->printInstantiations( out );
- }else{
- Assert(false);
- }
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ te->printInstantiations(out);
if (options::instFormatMode() == options::InstFormatMode::SZS)
{
out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
void SmtEngine::printSynthSolution( std::ostream& out ) {
SmtScope smts(this);
finishInit();
- if( d_theoryEngine ){
- d_theoryEngine->printSynthSolution( out );
- }else{
- Assert(false);
- }
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ te->printSynthSolution(out);
}
bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
SmtScope smts(this);
finishInit();
std::map<Node, std::map<Node, Node>> sol_mapn;
- Assert(d_theoryEngine != nullptr);
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
// fail if the theory engine does not have synthesis solutions
- if (!d_theoryEngine->getSynthSolutions(sol_mapn))
+ if (!te->getSynthSolutions(sol_mapn))
{
return false;
}
TypeNode t = NodeManager::currentNM()->booleanType();
Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
std::vector< Node > node_values;
- d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ te->setUserAttribute(
+ doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr);
n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr);
std::vector< Node > e_children;
Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl;
Assert(nn_e.getNumChildren() == 3);
- Result r = checkSatisfiability(nn_e.toExpr(), true, true);
+ Result r = checkSatInternal(std::vector<Node>{nn_e}, true, true);
Trace("smt-qe") << "Query returned " << r << std::endl;
if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) {
if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){
return e;
}
std::vector< Node > inst_qs;
- d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs );
+ te->getInstantiatedQuantifiedFormulas(inst_qs);
Assert(inst_qs.size() <= 1);
Node ret_n;
if( inst_qs.size()==1 ){
//Node top_q = Rewriter::rewrite( nn_e ).negate();
Assert(top_q.getKind() == kind::FORALL);
Trace("smt-qe") << "Get qe for " << top_q << std::endl;
- ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
+ ret_n = te->getInstantiatedConjunction(top_q);
Trace("smt-qe") << "Returned : " << ret_n << std::endl;
if (n_e.getKind() == kind::EXISTS)
{
void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
SmtScope smts(this);
- if( d_theoryEngine ){
- std::vector< Node > qs_n;
- d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n );
- for( unsigned i=0; i<qs_n.size(); i++ ){
- qs.push_back( qs_n[i].toExpr() );
- }
- }else{
- Assert(false);
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ std::vector<Node> qs_n;
+ te->getInstantiatedQuantifiedFormulas(qs_n);
+ for (std::size_t i = 0, n = qs_n.size(); i < n; i++)
+ {
+ qs.push_back(qs_n[i].toExpr());
}
}
void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
SmtScope smts(this);
- if( d_theoryEngine ){
- std::vector< Node > insts_n;
- d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n );
- for( unsigned i=0; i<insts_n.size(); i++ ){
- insts.push_back( insts_n[i].toExpr() );
- }
- }else{
- Assert(false);
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ std::vector<Node> insts_n;
+ te->getInstantiations(Node::fromExpr(q), insts_n);
+ for (std::size_t i = 0, n = insts_n.size(); i < n; i++)
+ {
+ insts.push_back(insts_n[i].toExpr());
}
}
void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) {
SmtScope smts(this);
Assert(options::trackInstLemmas());
- if( d_theoryEngine ){
- std::vector< std::vector< Node > > tvecs_n;
- d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n );
- for( unsigned i=0; i<tvecs_n.size(); i++ ){
- std::vector< Expr > tvec;
- for( unsigned j=0; j<tvecs_n[i].size(); j++ ){
- tvec.push_back( tvecs_n[i][j].toExpr() );
- }
- tvecs.push_back( tvec );
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ std::vector<std::vector<Node>> tvecs_n;
+ te->getInstantiationTermVectors(Node::fromExpr(q), tvecs_n);
+ for (std::size_t i = 0, n = tvecs_n.size(); i < n; i++)
+ {
+ std::vector<Expr> tvec;
+ for (std::size_t j = 0, m = tvecs_n[i].size(); j < m; j++)
+ {
+ tvec.push_back(tvecs_n[i][j].toExpr());
}
- }else{
- Assert(false);
+ tvecs.push_back(tvec);
}
}
finishInit();
d_state->doPendingPops();
Trace("smt") << "SMT push()" << endl;
- processAssertionsInternal();
+ d_smtSolver->processAssertions(*d_asserts);
if(Dump.isOn("benchmark")) {
Dump("benchmark") << PushCommand();
}
// push the state to maintain global context around everything
d_state->setup();
- /* Create new PropEngine.
- * First force destruction of referenced PropEngine to enforce that
- * statistics are unregistered by the obsolete PropEngine object before
- * registered again by the new PropEngine object */
- d_propEngine.reset(nullptr);
- d_propEngine.reset(new PropEngine(
- getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
- d_theoryEngine->setPropEngine(getPropEngine());
+ d_smtSolver->resetAssertions();
}
void SmtEngine::interrupt()
{
return;
}
- d_propEngine->interrupt();
- d_theoryEngine->interrupt();
+ d_smtSolver->interrupt();
}
void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
{
node_values.push_back( expr_values[i].getNode() );
}
- d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ te->setUserAttribute(attr, expr.getNode(), node_values, str_value);
}
void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
--- /dev/null
+/********************* */
+/*! \file smt_solver.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 solver for SMT queries in an SmtEngine.
+ **/
+
+#include "smt/smt_solver.h"
+
+#include "proof/theory_proof.h"
+#include "prop/prop_engine.h"
+#include "smt/assertions.h"
+#include "smt/preprocessor.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_state.h"
+#include "theory/theory_engine.h"
+#include "theory/theory_traits.h"
+
+namespace CVC4 {
+namespace smt {
+
+SmtSolver::SmtSolver(SmtEngine& smt,
+ SmtEngineState& state,
+ ResourceManager* rm,
+ Preprocessor& pp,
+ SmtEngineStatistics& stats)
+ : d_smt(smt),
+ d_state(state),
+ d_rm(rm),
+ d_pp(pp),
+ d_stats(stats),
+ d_theoryEngine(nullptr),
+ d_propEngine(nullptr)
+{
+}
+
+SmtSolver::~SmtSolver() {}
+
+void SmtSolver::finishInit(const LogicInfo& logicInfo)
+{
+ // We have mutual dependency here, so we add the prop engine to the theory
+ // engine later (it is non-essential there)
+ d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(),
+ d_smt.getUserContext(),
+ d_rm,
+ d_pp.getTermFormulaRemover(),
+ logicInfo));
+
+ // Add the theories
+ for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
+ ++id)
+ {
+ theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
+ // register with proof engine if applicable
+#ifdef CVC4_PROOF
+ ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(
+ d_theoryEngine->theoryOf(id));
+#endif
+ }
+
+ Trace("smt-debug") << "Making prop engine..." << std::endl;
+ /* force destruction of referenced PropEngine to enforce that statistics
+ * are unregistered by the obsolete PropEngine object before registered
+ * again by the new PropEngine object */
+ d_propEngine.reset(nullptr);
+ d_propEngine.reset(new PropEngine(
+ d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm));
+
+ Trace("smt-debug") << "Setting up theory engine..." << std::endl;
+ d_theoryEngine->setPropEngine(getPropEngine());
+ Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
+ d_theoryEngine->finishInit();
+}
+
+void SmtSolver::resetAssertions()
+{
+ /* Create new PropEngine.
+ * First force destruction of referenced PropEngine to enforce that
+ * statistics are unregistered by the obsolete PropEngine object before
+ * registered again by the new PropEngine object */
+ d_propEngine.reset(nullptr);
+ d_propEngine.reset(new PropEngine(
+ d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm));
+ d_theoryEngine->setPropEngine(getPropEngine());
+ // Notice that we do not reset TheoryEngine, nor does it require calling
+ // finishInit again. In particular, TheoryEngine::finishInit does not
+ // depend on knowing the associated PropEngine.
+}
+
+void SmtSolver::interrupt()
+{
+ if (d_propEngine != nullptr)
+ {
+ d_propEngine->interrupt();
+ }
+ if (d_theoryEngine != nullptr)
+ {
+ d_theoryEngine->interrupt();
+ }
+}
+
+void SmtSolver::shutdown()
+{
+ if (d_propEngine != nullptr)
+ {
+ d_propEngine->shutdown();
+ }
+ if (d_theoryEngine != nullptr)
+ {
+ d_theoryEngine->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
+ bool hasAssumptions = !assumptions.empty();
+ d_state.notifyCheckSat(hasAssumptions);
+
+ // then, initialize the assertions
+ as.initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
+
+ // make the check
+ Assert(d_smt.isFullyInited());
+
+ Trace("smt") << "SmtSolver::check()" << endl;
+
+ const std::string& filename = d_state.getFilename();
+ if (d_rm->out())
+ {
+ Result::UnknownExplanation why =
+ d_rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
+ return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
+ }
+ d_rm->beginCall();
+
+ // Make sure the prop layer has all of the assertions
+ Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
+ processAssertions(as);
+ Trace("smt") << "SmtSolver::check(): done processing assertions" << endl;
+
+ TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);
+
+ Chat() << "solving..." << endl;
+ Trace("smt") << "SmtSolver::check(): running check" << endl;
+ Result result = d_propEngine->checkSat();
+
+ d_rm->endCall();
+ Trace("limit") << "SmtSolver::check(): cumulative millis "
+ << d_rm->getTimeUsage() << ", resources "
+ << d_rm->getResourceUsage() << endl;
+
+ if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
+ && result.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ }
+ // flipped if we did a global negation
+ if (as.isGlobalNegated())
+ {
+ Trace("smt") << "SmtSolver::process global negate " << result << std::endl;
+ if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ result = Result(Result::SAT);
+ }
+ else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
+ {
+ // Only can answer unsat if the theory is satisfaction complete. This
+ // includes linear arithmetic and bitvectors, which are the primary
+ // targets for the global negate option. Other logics are possible here
+ // but not considered.
+ LogicInfo logic = d_smt.getLogicInfo();
+ if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) ||
+ logic.isPure(theory::THEORY_BV))
+ {
+ result = Result(Result::UNSAT);
+ }
+ else
+ {
+ result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ }
+ }
+ Trace("smt") << "SmtSolver::global negate returned " << result << std::endl;
+ }
+
+ // set the filename on the result
+ Result r = Result(result, filename);
+
+ // notify our state of the check-sat result
+ d_state.notifyCheckSatResult(hasAssumptions, r);
+
+ return r;
+}
+
+void SmtSolver::processAssertions(Assertions& as)
+{
+ TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
+ d_rm->spendResource(ResourceManager::Resource::PreprocessStep);
+ Assert(d_state.isFullyReady());
+
+ preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
+
+ if (ap.size() == 0)
+ {
+ // nothing to do
+ return;
+ }
+
+ // process the assertions with the preprocessor
+ bool noConflict = d_pp.process(as);
+
+ // notify theory engine new preprocessed assertions
+ d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
+
+ // Push the formula to decision engine
+ if (noConflict)
+ {
+ Chat() << "pushing to decision engine..." << endl;
+ d_propEngine->addAssertionsToDecisionEngine(ap);
+ }
+
+ // end: INVARIANT to maintain: no reordering of assertions or
+ // introducing new ones
+
+ d_pp.postprocess(as);
+
+ // Push the formula to SAT
+ {
+ Chat() << "converting to CNF..." << endl;
+ TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
+ for (const Node& assertion : ap.ref())
+ {
+ Chat() << "+ " << assertion << std::endl;
+ d_propEngine->assertFormula(assertion);
+ }
+ }
+
+ // clear the current assertions
+ as.clearCurrent();
+}
+
+TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
+
+prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file smt_solver.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 solver for SMT queries in an SmtEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__SMT_SOLVER_H
+#define CVC4__SMT__SMT_SOLVER_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/logic_info.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+class TheoryEngine;
+class ResourceManager;
+
+namespace prop {
+class PropEngine;
+}
+
+namespace smt {
+
+class Assertions;
+class SmtEngineState;
+class Preprocessor;
+class SmtEngineStatistics;
+
+/**
+ * A solver for SMT queries.
+ *
+ * This class manages the initialization of the theory engine and propositional
+ * engines and implements the method for checking satisfiability of the current
+ * set of assertions.
+ *
+ * Notice that this class is only conceptually responsible for running
+ * check-sat commands and an interface for sending formulas to the underlying
+ * classes. It does not implement any query techniques beyond getting the result
+ * (unsat/sat/unknown) of check-sat calls. More detailed information (e.g.
+ * models) can be queries using other classes that examine the state of the
+ * TheoryEngine directly, which can be accessed via getTheoryEngine.
+ */
+class SmtSolver
+{
+ public:
+ SmtSolver(SmtEngine& smt,
+ SmtEngineState& state,
+ ResourceManager* rm,
+ Preprocessor& pp,
+ SmtEngineStatistics& stats);
+ ~SmtSolver();
+ /**
+ * Create theory engine, prop engine based on the logic info.
+ */
+ void finishInit(const LogicInfo& logicInfo);
+ /** Reset all assertions, global declarations, etc. */
+ void resetAssertions();
+ /**
+ * Interrupt a running query. This can be called from another thread
+ * or from a signal handler. Throws a ModalException if the SmtSolver
+ * isn't currently in a query.
+ */
+ void interrupt();
+ /**
+ * This is called by the destructor of SmtEngine, just before destroying the
+ * PropEngine, TheoryEngine, and DecisionEngine (in that order). It
+ * is important because there are destruction ordering issues
+ * between PropEngine and Theory.
+ */
+ void shutdown();
+ /**
+ * Check satisfiability (used to check satisfiability and entailment)
+ * in SmtEngine. This is done via adding assumptions (when necessary) to
+ * assertions as, preprocessing and pushing assertions into the prop engine
+ * of this class, and checking for satisfiability via the prop engine.
+ *
+ * @param as The object managing the assertions in SmtEngine. This class
+ * maintains a current set of (unprocessed) assertions which are pushed
+ * into the internal members of this class (TheoryEngine and PropEngine)
+ * 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
+ * assertions that have been buffered into as, preprocesses them, pushes them
+ * into the SMT solver, and clears the buffer.
+ */
+ void processAssertions(Assertions& as);
+ //------------------------------------------ access methods
+ /** Get a pointer to the TheoryEngine owned by this solver. */
+ TheoryEngine* getTheoryEngine();
+ /** Get a pointer to the PropEngine owned by this solver. */
+ prop::PropEngine* getPropEngine();
+ //------------------------------------------ end access methods
+ private:
+ /** Reference to the parent SMT engine */
+ SmtEngine& d_smt;
+ /** Reference to the state of the SmtEngine */
+ SmtEngineState& d_state;
+ /** Pointer to a resource manager (owned by SmtEngine) */
+ ResourceManager* d_rm;
+ /** Reference to the preprocessor of SmtEngine */
+ Preprocessor& d_pp;
+ /** Reference to the statistics of SmtEngine */
+ SmtEngineStatistics& d_stats;
+ /** The theory engine */
+ std::unique_ptr<TheoryEngine> d_theoryEngine;
+ /** The propositional engine */
+ std::unique_ptr<prop::PropEngine> d_propEngine;
+};
+
+} // namespace smt
+} // namespace CVC4
+
+#endif /* CVC4__SMT__SMT_SOLVER_H */
projects / cvc5.git / commitdiff