std::istream& DriverOptions::in() const
{
- return *d_solver.d_smtEngine->getOptions().base.in;
+ return *d_solver.d_slv->getOptions().base.in;
}
std::ostream& DriverOptions::err() const
{
- return *d_solver.d_smtEngine->getOptions().base.err;
+ return *d_solver.d_slv->getOptions().base.err;
}
std::ostream& DriverOptions::out() const
{
- return *d_solver.d_smtEngine->getOptions().base.out;
+ return *d_solver.d_slv->getOptions().base.out;
}
/* -------------------------------------------------------------------------- */
d_nodeMgr = NodeManager::currentNM();
d_nodeMgr->init();
d_originalOptions = std::move(original);
- d_smtEngine.reset(new SmtEngine(d_nodeMgr, d_originalOptions.get()));
- d_smtEngine->setSolver(this);
- d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed));
+ d_slv.reset(new SolverEngine(d_nodeMgr, d_originalOptions.get()));
+ d_slv->setSolver(this);
+ d_rng.reset(new Random(d_slv->getOptions().driver.seed));
resetStatistics();
}
{
// Note: Term is checked in the caller to avoid double checks
//////// all checks before this line
- Node value = d_smtEngine->getValue(*term.d_node);
+ Node value = d_slv->getValue(*term.d_node);
Term res = Term(this, value);
// May need to wrap in real cast so that user know this is a real.
TypeNode tn = (*term.d_node).getType();
std::vector<Node> bvns = Term::termVectorToNodes(boundVars);
- d_smtEngine->declareSynthFun(
+ d_slv->declareSynthFun(
fun,
grammar == nullptr ? funType : *grammar->resolve().d_type,
isInv,
if constexpr (Configuration::isStatisticsBuild())
{
d_stats.reset(new APIStatistics{
- d_smtEngine->getStatisticsRegistry().registerHistogram<TypeConstant>(
+ d_slv->getStatisticsRegistry().registerHistogram<TypeConstant>(
"api::CONSTANT"),
- d_smtEngine->getStatisticsRegistry().registerHistogram<TypeConstant>(
+ d_slv->getStatisticsRegistry().registerHistogram<TypeConstant>(
"api::VARIABLE"),
- d_smtEngine->getStatisticsRegistry().registerHistogram<Kind>(
- "api::TERM"),
+ d_slv->getStatisticsRegistry().registerHistogram<Kind>("api::TERM"),
});
}
}
void Solver::printStatisticsSafe(int fd) const
{
- d_smtEngine->printStatisticsSafe(fd);
+ d_slv->printStatisticsSafe(fd);
}
/* Helpers for mkTerm checks. */
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_SOLVER_CHECK_TERM(term);
//////// all checks before this line
- return Term(this, d_smtEngine->simplify(*term.d_node));
+ return Term(this, d_slv->simplify(*term.d_node));
////////
CVC5_API_TRY_CATCH_END;
}
Result Solver::checkEntailed(const Term& term) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(!d_smtEngine->isQueryMade()
- || d_smtEngine->getOptions().base.incrementalSolving)
+ CVC5_API_CHECK(!d_slv->isQueryMade()
+ || d_slv->getOptions().base.incrementalSolving)
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
CVC5_API_SOLVER_CHECK_TERM(term);
//////// all checks before this line
- return d_smtEngine->checkEntailed(*term.d_node);
+ return d_slv->checkEntailed(*term.d_node);
////////
CVC5_API_TRY_CATCH_END;
}
Result Solver::checkEntailed(const std::vector<Term>& terms) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(!d_smtEngine->isQueryMade()
- || d_smtEngine->getOptions().base.incrementalSolving)
+ CVC5_API_CHECK(!d_slv->isQueryMade()
+ || d_slv->getOptions().base.incrementalSolving)
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
CVC5_API_SOLVER_CHECK_TERMS(terms);
//////// all checks before this line
- return d_smtEngine->checkEntailed(Term::termVectorToNodes(terms));
+ return d_slv->checkEntailed(Term::termVectorToNodes(terms));
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_SOLVER_CHECK_TERM(term);
CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term, getBooleanSort());
//////// all checks before this line
- d_smtEngine->assertFormula(*term.d_node);
+ d_slv->assertFormula(*term.d_node);
////////
CVC5_API_TRY_CATCH_END;
}
Result Solver::checkSat(void) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(!d_smtEngine->isQueryMade()
- || d_smtEngine->getOptions().base.incrementalSolving)
+ CVC5_API_CHECK(!d_slv->isQueryMade()
+ || d_slv->getOptions().base.incrementalSolving)
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
//////// all checks before this line
- return d_smtEngine->checkSat();
+ return d_slv->checkSat();
////////
CVC5_API_TRY_CATCH_END;
}
Result Solver::checkSatAssuming(const Term& assumption) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(!d_smtEngine->isQueryMade()
- || d_smtEngine->getOptions().base.incrementalSolving)
+ CVC5_API_CHECK(!d_slv->isQueryMade()
+ || d_slv->getOptions().base.incrementalSolving)
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort());
//////// all checks before this line
- return d_smtEngine->checkSat(*assumption.d_node);
+ return d_slv->checkSat(*assumption.d_node);
////////
CVC5_API_TRY_CATCH_END;
}
Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
- || d_smtEngine->getOptions().base.incrementalSolving)
+ CVC5_API_CHECK(!d_slv->isQueryMade() || assumptions.size() == 0
+ || d_slv->getOptions().base.incrementalSolving)
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort());
CVC5_API_SOLVER_CHECK_TERM(term);
}
std::vector<Node> eassumptions = Term::termVectorToNodes(assumptions);
- return d_smtEngine->checkSat(eassumptions);
+ return d_slv->checkSat(eassumptions);
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts);
//////// all checks before this line
- d_smtEngine->defineFunction(
+ d_slv->defineFunction(
*fun.d_node, Term::termVectorToNodes(bound_vars), *term.d_node, global);
return fun;
////////
}
//////// all checks before this line
std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
- d_smtEngine->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global);
+ d_slv->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global);
return fun;
////////
CVC5_API_TRY_CATCH_END;
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
+ CVC5_API_CHECK(d_slv->getUserLogicInfo().isQuantified())
<< "recursive function definitions require a logic with quantifiers";
- CVC5_API_CHECK(
- d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
+ CVC5_API_CHECK(d_slv->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
<< "recursive function definitions require a logic with uninterpreted "
"functions";
CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts);
//////// all checks before this line
- d_smtEngine->defineFunctionRec(
+ d_slv->defineFunctionRec(
*fun.d_node, Term::termVectorToNodes(bound_vars), *term.d_node, global);
return fun;
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
+ CVC5_API_CHECK(d_slv->getUserLogicInfo().isQuantified())
<< "recursive function definitions require a logic with quantifiers";
- CVC5_API_CHECK(
- d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
+ CVC5_API_CHECK(d_slv->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
<< "recursive function definitions require a logic with uninterpreted "
"functions";
//////// all checks before this line
std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
- d_smtEngine->defineFunctionRec(
- *fun.d_node, ebound_vars, *term.d_node, global);
+ d_slv->defineFunctionRec(*fun.d_node, ebound_vars, *term.d_node, global);
return fun;
////////
CVC5_API_TRY_CATCH_END;
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
+ CVC5_API_CHECK(d_slv->getUserLogicInfo().isQuantified())
<< "recursive function definitions require a logic with quantifiers";
- CVC5_API_CHECK(
- d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
+ CVC5_API_CHECK(d_slv->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
<< "recursive function definitions require a logic with uninterpreted "
"functions";
CVC5_API_SOLVER_CHECK_TERMS(funs);
ebound_vars.push_back(Term::termVectorToNodes(v));
}
std::vector<Node> nodes = Term::termVectorToNodes(terms);
- d_smtEngine->defineFunctionsRec(efuns, ebound_vars, nodes, global);
+ d_slv->defineFunctionsRec(efuns, ebound_vars, nodes, global);
////////
CVC5_API_TRY_CATCH_END;
}
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- std::vector<Node> assertions = d_smtEngine->getAssertions();
+ std::vector<Node> assertions = d_slv->getAssertions();
/* Can not use
* return std::vector<Term>(assertions.begin(), assertions.end());
* here since constructor is private */
std::string Solver::getInfo(const std::string& flag) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag))
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isValidGetInfoFlag(flag))
<< "Unrecognized flag for getInfo.";
//////// all checks before this line
- return d_smtEngine->getInfo(flag);
+ return d_slv->getInfo(flag);
////////
CVC5_API_TRY_CATCH_END;
}
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- return d_smtEngine->getOption(option);
+ return d_slv->getOption(option);
////////
CVC5_API_TRY_CATCH_END;
}
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- auto info = options::getInfo(d_smtEngine->getOptions(), option);
+ auto info = options::getInfo(d_slv->getOptions(), option);
CVC5_API_CHECK(info.name != "")
<< "Querying invalid or unknown option " << option;
return std::visit(
std::vector<Term> Solver::getUnsatAssumptions(void) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
+ CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
<< "Cannot get unsat assumptions unless incremental solving is enabled "
"(try --incremental)";
- CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions)
+ CVC5_API_CHECK(d_slv->getOptions().smt.unsatAssumptions)
<< "Cannot get unsat assumptions unless explicitly enabled "
"(try --produce-unsat-assumptions)";
- CVC5_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
+ CVC5_API_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT)
<< "Cannot get unsat assumptions unless in unsat mode.";
//////// all checks before this line
- std::vector<Node> uassumptions = d_smtEngine->getUnsatAssumptions();
+ std::vector<Node> uassumptions = d_slv->getUnsatAssumptions();
/* Can not use
* return std::vector<Term>(uassumptions.begin(), uassumptions.end());
* here since constructor is private */
std::vector<Term> Solver::getUnsatCore(void) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores)
+ CVC5_API_CHECK(d_slv->getOptions().smt.unsatCores)
<< "Cannot get unsat core unless explicitly enabled "
"(try --produce-unsat-cores)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
+ CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT)
<< "Cannot get unsat core unless in unsat mode.";
//////// all checks before this line
- UnsatCore core = d_smtEngine->getUnsatCore();
+ UnsatCore core = d_slv->getUnsatCore();
/* Can not use
* return std::vector<Term>(core.begin(), core.end());
* here since constructor is private */
std::map<Term, Term> Solver::getDifficulty() const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT
- || d_smtEngine->getSmtMode() == SmtMode::SAT
- || d_smtEngine->getSmtMode()
- == SmtMode::SAT_UNKNOWN)
+ CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT
+ || d_slv->getSmtMode() == SmtMode::SAT
+ || d_slv->getSmtMode() == SmtMode::SAT_UNKNOWN)
<< "Cannot get difficulty unless after a UNSAT, SAT or unknown response.";
//////// all checks before this line
std::map<Term, Term> res;
std::map<Node, Node> dmap;
- d_smtEngine->getDifficultyMap(dmap);
+ d_slv->getDifficultyMap(dmap);
for (const std::pair<const Node, Node>& d : dmap)
{
res[Term(this, d.first)] = Term(this, d.second);
std::string Solver::getProof(void) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceProofs)
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceProofs)
<< "Cannot get proof explicitly enabled (try --produce-proofs)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
+ CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT)
<< "Cannot get proof unless in unsat mode.";
- return d_smtEngine->getProof();
+ return d_slv->getProof();
CVC5_API_TRY_CATCH_END;
}
std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Cannot get value unless after a SAT or unknown response.";
CVC5_API_SOLVER_CHECK_TERMS(terms);
//////// all checks before this line
std::vector<Term> Solver::getModelDomainElements(const Sort& s) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot get domain elements unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Cannot get domain elements unless after a SAT or unknown response.";
CVC5_API_SOLVER_CHECK_SORT(s);
CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort())
"getModelDomainElements.";
//////// all checks before this line
std::vector<Term> res;
- std::vector<Node> elements =
- d_smtEngine->getModelDomainElements(s.getTypeNode());
+ std::vector<Node> elements = d_slv->getModelDomainElements(s.getTypeNode());
for (const Node& n : elements)
{
res.push_back(Term(this, n));
bool Solver::isModelCoreSymbol(const Term& v) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot check if model core symbol unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Cannot check if model core symbol unless after a SAT or unknown "
"response.";
CVC5_API_SOLVER_CHECK_TERM(v);
CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT)
<< "Expecting a free constant as argument to isModelCoreSymbol.";
//////// all checks before this line
- return d_smtEngine->isModelCoreSymbol(v.getNode());
+ return d_slv->isModelCoreSymbol(v.getNode());
////////
CVC5_API_TRY_CATCH_END;
}
const std::vector<Term>& vars) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot get model unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Cannot get model unless after a SAT or unknown response.";
CVC5_API_SOLVER_CHECK_SORTS(sorts);
for (const Sort& s : sorts)
<< "Expecting a free constant as argument to getModel.";
}
//////// all checks before this line
- return d_smtEngine->getModel(Sort::sortVectorToTypeNodes(sorts),
- Term::termVectorToNodes(vars));
+ return d_slv->getModel(Sort::sortVectorToTypeNodes(sorts),
+ Term::termVectorToNodes(vars));
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_SOLVER_CHECK_TERM(q);
//////// all checks before this line
- return Term(this,
- d_smtEngine->getQuantifierElimination(q.getNode(), true, true));
+ return Term(this, d_slv->getQuantifierElimination(q.getNode(), true, true));
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_SOLVER_CHECK_TERM(q);
//////// all checks before this line
- return Term(this,
- d_smtEngine->getQuantifierElimination(q.getNode(), false, true));
+ return Term(this, d_slv->getQuantifierElimination(q.getNode(), false, true));
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_SOLVER_CHECK_SORT(locSort);
CVC5_API_SOLVER_CHECK_SORT(dataSort);
- CVC5_API_CHECK(
- d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
+ CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
<< "Cannot obtain separation logic expressions if not using the "
"separation logic theory.";
//////// all checks before this line
- d_smtEngine->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode());
+ d_slv->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode());
////////
CVC5_API_TRY_CATCH_END;
}
Term Solver::getSeparationHeap() const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(
- d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
+ CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
<< "Cannot obtain separation logic expressions if not using the "
"separation logic theory.";
- CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot get separation heap term unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Can only get separtion heap term after sat or unknown response.";
//////// all checks before this line
- return Term(this, d_smtEngine->getSepHeapExpr());
+ return Term(this, d_slv->getSepHeapExpr());
////////
CVC5_API_TRY_CATCH_END;
}
Term Solver::getSeparationNilTerm() const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(
- d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
+ CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
<< "Cannot obtain separation logic expressions if not using the "
"separation logic theory.";
- CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot get separation nil term unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Can only get separtion nil term after sat or unknown response.";
//////// all checks before this line
- return Term(this, d_smtEngine->getSepNilExpr());
+ return Term(this, d_slv->getSepNilExpr());
////////
CVC5_API_TRY_CATCH_END;
}
TypeNode setType = getNodeManager()->mkSetType(*sort.d_type);
Node pool = getNodeManager()->mkBoundVar(symbol, setType);
std::vector<Node> initv = Term::termVectorToNodes(initValue);
- d_smtEngine->declarePool(pool, initv);
+ d_slv->declarePool(pool, initv);
return Term(this, pool);
////////
CVC5_API_TRY_CATCH_END;
void Solver::pop(uint32_t nscopes) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
+ CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
<< "Cannot pop when not solving incrementally (use --incremental)";
- CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels())
+ CVC5_API_CHECK(nscopes <= d_slv->getNumUserLevels())
<< "Cannot pop beyond first pushed context";
//////// all checks before this line
for (uint32_t n = 0; n < nscopes; ++n)
{
- d_smtEngine->pop();
+ d_slv->pop();
}
////////
CVC5_API_TRY_CATCH_END;
CVC5_API_SOLVER_CHECK_TERM(conj);
//////// all checks before this line
Node result;
- bool success = d_smtEngine->getInterpol(*conj.d_node, result);
+ bool success = d_slv->getInterpol(*conj.d_node, result);
if (success)
{
output = Term(this, result);
//////// all checks before this line
Node result;
bool success =
- d_smtEngine->getInterpol(*conj.d_node, *grammar.resolve().d_type, result);
+ d_slv->getInterpol(*conj.d_node, *grammar.resolve().d_type, result);
if (success)
{
output = Term(this, result);
CVC5_API_SOLVER_CHECK_TERM(conj);
//////// all checks before this line
Node result;
- bool success = d_smtEngine->getAbduct(*conj.d_node, result);
+ bool success = d_slv->getAbduct(*conj.d_node, result);
if (success)
{
output = Term(this, result);
//////// all checks before this line
Node result;
bool success =
- d_smtEngine->getAbduct(*conj.d_node, *grammar.resolve().d_type, result);
+ d_slv->getAbduct(*conj.d_node, *grammar.resolve().d_type, result);
if (success)
{
output = Term(this, result);
void Solver::blockModel() const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Can only block model after sat or unknown response.";
//////// all checks before this line
- d_smtEngine->blockModel();
+ d_slv->blockModel();
////////
CVC5_API_TRY_CATCH_END;
}
void Solver::blockModelValues(const std::vector<Term>& terms) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceModels)
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
- CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
<< "Can only block model values after sat or unknown response.";
CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
<< "a non-empty set of terms";
CVC5_API_SOLVER_CHECK_TERMS(terms);
//////// all checks before this line
- d_smtEngine->blockModelValues(Term::termVectorToNodes(terms));
+ d_slv->blockModelValues(Term::termVectorToNodes(terms));
////////
CVC5_API_TRY_CATCH_END;
}
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- d_smtEngine->printInstantiations(out);
+ d_slv->printInstantiations(out);
////////
CVC5_API_TRY_CATCH_END;
}
void Solver::push(uint32_t nscopes) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
+ CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
<< "Cannot push when not solving incrementally (use --incremental)";
//////// all checks before this line
for (uint32_t n = 0; n < nscopes; ++n)
{
- d_smtEngine->push();
+ d_slv->push();
}
////////
CVC5_API_TRY_CATCH_END;
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- d_smtEngine->resetAssertions();
+ d_slv->resetAssertions();
////////
CVC5_API_TRY_CATCH_END;
}
value)
<< "'sat', 'unsat' or 'unknown'";
//////// all checks before this line
- d_smtEngine->setInfo(keyword, value);
+ d_slv->setInfo(keyword, value);
////////
CVC5_API_TRY_CATCH_END;
}
void Solver::setLogic(const std::string& logic) const
{
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(!d_smtEngine->isFullyInited())
+ CVC5_API_CHECK(!d_slv->isFullyInited())
<< "Invalid call to 'setLogic', solver is already fully initialized";
cvc5::LogicInfo logic_info(logic);
//////// all checks before this line
- d_smtEngine->setLogic(logic_info);
+ d_slv->setLogic(logic_info);
////////
CVC5_API_TRY_CATCH_END;
}
if (std::find(mutableOpts.begin(), mutableOpts.end(), option)
== mutableOpts.end())
{
- CVC5_API_CHECK(!d_smtEngine->isFullyInited())
+ CVC5_API_CHECK(!d_slv->isFullyInited())
<< "Invalid call to 'setOption' for option '" << option
<< "', solver is already fully initialized";
}
//////// all checks before this line
- d_smtEngine->setOption(option, value);
+ d_slv->setOption(option, value);
////////
CVC5_API_TRY_CATCH_END;
}
Node res = getNodeManager()->mkBoundVar(symbol, *sort.d_type);
(void)res.getType(true); /* kick off type checking */
- d_smtEngine->declareSygusVar(res);
+ d_slv->declareSygusVar(res);
return Term(this, res);
////////
term.d_node->getType() == getNodeManager()->booleanType(), term)
<< "boolean term";
//////// all checks before this line
- d_smtEngine->assertSygusConstraint(*term.d_node, false);
+ d_slv->assertSygusConstraint(*term.d_node, false);
////////
CVC5_API_TRY_CATCH_END;
}
term.d_node->getType() == getNodeManager()->booleanType(), term)
<< "boolean term";
//////// all checks before this line
- d_smtEngine->assertSygusConstraint(*term.d_node, true);
+ d_slv->assertSygusConstraint(*term.d_node, true);
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_CHECK(trans.d_node->getType() == expectedTransType)
<< "Expected trans's sort to be " << invType;
- d_smtEngine->assertSygusInvConstraint(
+ d_slv->assertSygusInvConstraint(
*inv.d_node, *pre.d_node, *trans.d_node, *post.d_node);
////////
CVC5_API_TRY_CATCH_END;
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- return d_smtEngine->checkSynth();
+ return d_slv->checkSynth();
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_SOLVER_CHECK_TERM(term);
std::map<cvc5::Node, cvc5::Node> map;
- CVC5_API_CHECK(d_smtEngine->getSynthSolutions(map))
+ CVC5_API_CHECK(d_slv->getSynthSolutions(map))
<< "The solver is not in a state immediately preceded by a "
"successful call to checkSynth";
CVC5_API_SOLVER_CHECK_TERMS(terms);
std::map<cvc5::Node, cvc5::Node> map;
- CVC5_API_CHECK(d_smtEngine->getSynthSolutions(map))
+ CVC5_API_CHECK(d_slv->getSynthSolutions(map))
<< "The solver is not in a state immediately preceded by a "
"successful call to checkSynth";
//////// all checks before this line
Statistics Solver::getStatistics() const
{
- return Statistics(d_smtEngine->getStatisticsRegistry());
+ return Statistics(d_slv->getStatisticsRegistry());
}
bool Solver::isOutputOn(const std::string& tag) const
// here but roll our own.
try
{
- return d_smtEngine->getEnv().isOutputOn(tag);
+ return d_slv->getEnv().isOutputOn(tag);
}
catch (const cvc5::Exception& e)
{
// here but roll our own.
try
{
- return d_smtEngine->getEnv().getOutput(tag);
+ return d_slv->getEnv().getOutput(tag);
}
catch (const cvc5::Exception& e)
{
class DTypeConstructor;
class DTypeSelector;
class NodeManager;
-class SmtEngine;
+class SolverEngine;
class TypeNode;
class Options;
class Random;
/** The statistics collected on the Api level. */
std::unique_ptr<APIStatistics> d_stats;
/** The SMT engine of this solver. */
- std::unique_ptr<SmtEngine> d_smtEngine;
+ std::unique_ptr<SolverEngine> d_slv;
/** The random number generator of this solver. */
std::unique_ptr<Random> d_rng;
};
virtual prop::SatLiteral getNextInternal(bool& stopSearch) = 0;
/** Pointer to the SAT context */
context::Context* d_context;
- /** Pointer to resource manager for associated SmtEngine */
+ /** Pointer to resource manager for associated SolverEngine */
ResourceManager* d_resourceManager;
/** Pointer to the CNF stream */
prop::CnfStream* d_cnfStream;
}
/**
- * This is called by SmtEngine, at shutdown time, just before
+ * This is called by SolverEngine, at shutdown time, just before
* destruction. It is important because there are destruction
* ordering issues between some parts of the system.
*/
void CommandExecutor::storeOptionsAsOriginal()
{
- d_solver->d_originalOptions->copyValues(d_solver->d_smtEngine->getOptions());
+ d_solver->d_originalOptions->copyValues(d_solver->d_slv->getOptions());
}
void CommandExecutor::printStatistics(std::ostream& out) const
}
// We can't really clear out the sequence and abort the current line,
// because the parse error might be for the second command on the
- // line. The first ones haven't yet been executed by the SmtEngine,
+ // line. The first ones haven't yet been executed by the SolverEngine,
// but the parser state has already made the variables and the mappings
// in the symbol table. So unfortunately, either we exit cvc5 entirely,
// or we commit to the current line up to the command with the parse
+ aMod2PlusbMod2Div2));
}
-OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
+OptimizationResult OMTOptimizerBitVector::minimize(SolverEngine* optChecker,
TNode target)
{
// the smt engine to which we send intermediate queries
return OptimizationResult(lastSatResult, value);
}
-OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
+OptimizationResult OMTOptimizerBitVector::maximize(SolverEngine* optChecker,
TNode target)
{
// the smt engine to which we send intermediate queries
public:
OMTOptimizerBitVector(bool isSigned);
virtual ~OMTOptimizerBitVector() = default;
- smt::OptimizationResult minimize(SmtEngine* optChecker,
+ smt::OptimizationResult minimize(SolverEngine* optChecker,
TNode target) override;
- smt::OptimizationResult maximize(SmtEngine* optChecker,
+ smt::OptimizationResult maximize(SolverEngine* optChecker,
TNode target) override;
private:
using namespace cvc5::smt;
namespace cvc5::omt {
-OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
+OptimizationResult OMTOptimizerInteger::optimize(SolverEngine* optChecker,
TNode target,
bool isMinimize)
{
return OptimizationResult(lastSatResult, value);
}
-OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker,
+OptimizationResult OMTOptimizerInteger::minimize(SolverEngine* optChecker,
TNode target)
{
return this->optimize(optChecker, target, true);
}
-OptimizationResult OMTOptimizerInteger::maximize(SmtEngine* optChecker,
+OptimizationResult OMTOptimizerInteger::maximize(SolverEngine* optChecker,
TNode target)
{
return this->optimize(optChecker, target, false);
public:
OMTOptimizerInteger() = default;
virtual ~OMTOptimizerInteger() = default;
- smt::OptimizationResult minimize(SmtEngine* optChecker,
+ smt::OptimizationResult minimize(SolverEngine* optChecker,
TNode target) override;
- smt::OptimizationResult maximize(SmtEngine* optChecker,
+ smt::OptimizationResult maximize(SolverEngine* optChecker,
TNode target) override;
private:
* isMinimize = true will trigger minimization,
* otherwise trigger maximization
**/
- smt::OptimizationResult optimize(SmtEngine* optChecker,
+ smt::OptimizationResult optimize(SolverEngine* optChecker,
TNode target,
bool isMinimize);
};
* @return smt::OptimizationResult the result of optimization, containing
* whether it's optimal and the optimized value.
**/
- virtual smt::OptimizationResult minimize(SmtEngine* optChecker,
+ virtual smt::OptimizationResult minimize(SolverEngine* optChecker,
TNode target) = 0;
/**
* Maximize the target node with constraints encoded in optChecker
* @return smt::OptimizationResult the result of optimization, containing
* whether it's optimal and the optimized value.
**/
- virtual smt::OptimizationResult maximize(SmtEngine* optChecker,
+ virtual smt::OptimizationResult maximize(SolverEngine* optChecker,
TNode target) = 0;
};
{ cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr)));
// Ugly that this changes the state of the parser; but
// global-declarations affects parsing, so we can't hold off
- // on this until some SmtEngine eventually (if ever) executes it.
+ // on this until some SolverEngine eventually (if ever) executes it.
if(name == ":global-declarations")
{
SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true");
: SIMPLE_SYMBOL
{ id = AntlrInput::tokenText($SIMPLE_SYMBOL);
if(!PARSER_STATE->isAbstractValue(id)) {
- // if an abstract value, SmtEngine handles declaration
+ // if an abstract value, SolverEngine handles declaration
PARSER_STATE->checkDeclaration(id, check, type);
}
}
/* strip off the quotes */
id = id.substr(1, id.size() - 2);
if(!PARSER_STATE->isAbstractValue(id)) {
- // if an abstract value, SmtEngine handles declaration
+ // if an abstract value, SolverEngine handles declaration
PARSER_STATE->checkDeclaration(id, check, type);
}
}
{
// If not from a command, just set the logic directly. Notice this is
// important since we do not want to enqueue a set-logic command and
- // fully initialize the underlying SmtEngine in the meantime before the
+ // fully initialize the underlying SolverEngine in the meantime before the
// command has a chance to execute, which would lead to an error.
d_solver->setLogic(logic);
return nullptr;
AssertionPipeline* assertionsToPreprocess)
{
Chat() << "applying substitutions..." << std::endl;
- Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
+ Trace("apply-substs") << "ApplySubsts::processAssertions(): "
<< "applying substitutions" << std::endl;
// TODO(#1255): Substitutions in incremental mode should be managed with a
// proper data structure.
Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl;
// make a separate smt call
- std::unique_ptr<SmtEngine> rrSygus;
+ std::unique_ptr<SolverEngine> rrSygus;
theory::initializeSubsolver(rrSygus, options(), logicInfo());
rrSygus->assertFormula(body);
Trace("sygus-infer") << "*** Check sat..." << std::endl;
namespace preprocessing {
PreprocessingPassContext::PreprocessingPassContext(
- SmtEngine* smt,
+ SolverEngine* slv,
Env& env,
theory::booleans::CircuitPropagator* circuitPropagator)
: EnvObj(env),
- d_smt(smt),
+ d_slv(slv),
d_circuitPropagator(circuitPropagator),
d_llm(
env.getTopLevelSubstitutions(), userContext(), getProofNodeManager()),
TheoryEngine* PreprocessingPassContext::getTheoryEngine() const
{
- return d_smt->getTheoryEngine();
+ return d_slv->getTheoryEngine();
}
prop::PropEngine* PreprocessingPassContext::getPropEngine() const
{
- return d_smt->getPropEngine();
+ return d_slv->getPropEngine();
}
void PreprocessingPassContext::spendResource(Resource r)
namespace cvc5 {
class Env;
-class SmtEngine;
+class SolverEngine;
class TheoryEngine;
namespace theory::booleans {
public:
/** Constructor. */
PreprocessingPassContext(
- SmtEngine* smt,
+ SolverEngine* smt,
Env& env,
theory::booleans::CircuitPropagator* circuitPropagator);
ProofNodeManager* getProofNodeManager() const;
private:
- /** Pointer to the SmtEngine that this context was created in. */
- SmtEngine* d_smt;
+ /** Pointer to the SolverEngine that this context was created in. */
+ SolverEngine* d_slv;
/** Instance of the circuit propagator */
theory::booleans::CircuitPropagator* d_circuitPropagator;
/**
void toStream(std::ostream& out, const smt::Model& m) const override;
/**
* Writes the unsat core to the stream out.
- * We use the expression names that are stored in the SMT engine associated
- * with the core (UnsatCore::getSmtEngine) for printing named assertions.
+ * We use the expression names that are associated with the core
+ * (UnsatCore::getCoreNames) for printing named assertions.
*/
void toStream(std::ostream& out, const UnsatCore& core) const override;
size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
- /** print unsat core to stream
- * We use the expression names stored in the SMT engine associated with the
- * unsat core with UnsatCore::getSmtEngine.
+ /**
+ * Print unsat core to stream.
+ * We use the expression names associated with the unsat core
+ * (UnsatCore::getCoreNames).
*/
void toStream(std::ostream& out, const UnsatCore& core) const override;
*/
SatLiteral convertAtom(TNode node);
- /** Pointer to resource manager for associated SmtEngine */
+ /** Pointer to resource manager for associated SolverEngine */
ResourceManager* d_resourceManager;
private:
================ CHANGES TO THE ORIGINAL CODE ==================================
The only cvc5 connections passed to minisat are the proxy (defined in sat.h) and
-the context. The context is obtained from the SmtEngine, and the proxy is an
+the context. The context is obtained from the SolverEngine, and the proxy is an
intermediary class that has all-access to the SatSolver so as to simplify the
interface to (possible) other sat solvers. These two are passed to minisat at
construction time and some additional flags are set. We use the SimpSolver
void finishInit();
/**
- * This is called by SmtEngine, at shutdown time, just before
+ * This is called by SolverEngine, at shutdown time, just before
* destruction. It is important because there are destruction
* ordering issues between some parts of the system (notably between
* PropEngine and Theory). For now, there's nothing to do here in
const char* msg = "Cannot get abduct when produce-abducts options is off.";
throw ModalException(msg);
}
- Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl;
+ Trace("sygus-abduct") << "SolverEngine::getAbduct: goal " << goal
+ << std::endl;
std::vector<Node> asserts(axioms.begin(), axioms.end());
// must expand definitions
Node conjn = d_env.getTopLevelSubstitutions().apply(goal);
Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1);
// remember the abduct-to-synthesize
d_sssf = aconj[0][0];
- Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
- << ", solving for " << d_sssf << std::endl;
+ Trace("sygus-abduct") << "SolverEngine::getAbduct: made conjecture : "
+ << aconj << ", solving for " << d_sssf << std::endl;
// we generate a new smt engine to do the abduction query
initializeSubsolver(d_subsolver, d_env);
// get the logic
{
// should have initialized the subsolver by now
Assert(d_subsolver != nullptr);
- Trace("sygus-abduct") << " SmtEngine::getAbduct check sat..." << std::endl;
+ Trace("sygus-abduct") << " SolverEngine::getAbduct check sat..."
+ << std::endl;
Result r = d_subsolver->checkSat();
- Trace("sygus-abduct") << " SmtEngine::getAbduct result: " << r << std::endl;
+ Trace("sygus-abduct") << " SolverEngine::getAbduct result: " << r
+ << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
// get the synthesis solution
std::map<Node, Node>::iterator its = sols.find(d_sssf);
if (its != sols.end())
{
- Trace("sygus-abduct")
- << "SmtEngine::getAbduct: solution is " << its->second << std::endl;
+ Trace("sygus-abduct") << "SolverEngine::getAbduct: solution is "
+ << its->second << std::endl;
abd = its->second;
if (abd.getKind() == kind::LAMBDA)
{
}
return true;
}
- Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!"
+ Trace("sygus-abduct") << "SolverEngine::getAbduct: could not find solution!"
<< std::endl;
throw RecoverableModalException("Could not find solution for get-abduct.");
}
void AbductionSolver::checkAbduct(const std::vector<Node>& axioms, Node a)
{
Assert(a.getType().isBoolean());
- Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions"
+ Trace("check-abduct") << "SolverEngine::checkAbduct: get expanded assertions"
<< std::endl;
std::vector<Node> asserts(axioms.begin(), axioms.end());
// is unsatisfiable.
for (unsigned j = 0; j < 2; j++)
{
- Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+ Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j
<< ": make new SMT engine" << std::endl;
// Start new SMT engine to check solution
- std::unique_ptr<SmtEngine> abdChecker;
+ std::unique_ptr<SolverEngine> abdChecker;
initializeSubsolver(abdChecker, d_env);
- Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+ Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j
<< ": asserting formulas" << std::endl;
for (const Node& e : asserts)
{
abdChecker->assertFormula(e);
}
- Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+ Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j
<< ": check the assertions" << std::endl;
Result r = abdChecker->checkSat();
- Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+ Trace("check-abduct") << "SolverEngine::checkAbduct: phase " << j
<< ": result is " << r << std::endl;
std::stringstream serr;
bool isError = false;
if (r.asSatisfiabilityResult().isSat() != Result::SAT)
{
isError = true;
- serr << "SmtEngine::checkAbduct(): produced solution cannot be shown "
- "to be consisconsistenttent with assertions, result was "
- << r;
+ serr
+ << "SolverEngine::checkAbduct(): produced solution cannot be shown "
+ "to be consisconsistenttent with assertions, result was "
+ << r;
}
Trace("check-abduct")
- << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl;
+ << "SolverEngine::checkAbduct: goal is " << d_abdConj << std::endl;
// add the goal to the set of assertions
Assert(!d_abdConj.isNull());
asserts.push_back(d_abdConj);
if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
{
isError = true;
- serr << "SmtEngine::checkAbduct(): negated goal cannot be shown "
+ serr << "SolverEngine::checkAbduct(): negated goal cannot be shown "
"unsatisfiable with produced solution, result was "
<< r;
}
namespace cvc5 {
-class SmtEngine;
+class SolverEngine;
namespace smt {
* A solver for abduction queries.
*
* This class is responsible for responding to get-abduct commands. It spawns
- * a subsolver SmtEngine for a sygus conjecture that captures the abduction
+ * a subsolver SolverEngine for a sygus conjecture that captures the abduction
* query, and implements supporting utility methods such as checkAbduct.
*/
class AbductionSolver : protected EnvObj
* assertion stack unchaged. This copy of the SMT engine can be further
* queried for information regarding further solutions.
*/
- std::unique_ptr<SmtEngine> d_subsolver;
+ std::unique_ptr<SolverEngine> d_subsolver;
/**
* The conjecture of the current abduction problem. This expression is only
- * valid while the parent SmtEngine is in mode SMT_MODE_ABDUCT.
+ * valid while the parent SolverEngine is in mode SMT_MODE_ABDUCT.
*/
Node d_abdConj;
/**
// true, nothing to do
return;
}
- Trace("smt") << "SmtEnginePrivate::addFormula(" << n
- << ", inInput = " << inInput
+ Trace("smt") << "Assertions::addFormula(" << n << ", inInput = " << inInput
<< ", isAssumption = " << isAssumption
<< ", isFunDef = " << isFunDef << std::endl;
if (isFunDef)
// Now go through all our user assertions checking if they're satisfied.
for (const Node& assertion : *al)
{
- Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
+ Notice() << "SolverEngine::checkModel(): checking assertion " << assertion
<< std::endl;
// Apply any define-funs from the problem. We do not expand theory symbols
// is not trustworthy, since the UF introduced by expanding definitions may
// not be properly constrained.
Node n = sm.apply(assertion, false);
- Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << std::endl;
+ Notice() << "SolverEngine::checkModel(): -- substitutes to " << n
+ << std::endl;
n = Rewriter::rewrite(n);
- Notice() << "SmtEngine::checkModel(): -- rewrites to " << n << std::endl;
+ Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl;
// We look up the value before simplifying. If n contains quantifiers,
// this may increases the chance of finding its value before the node is
// altered by simplification below.
n = m->getValue(n);
- Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
+ Notice() << "SolverEngine::checkModel(): -- get value : " << n << std::endl;
if (n.isConst() && n.getConst<bool>())
{
if (!n.isConst())
{
// Not constant, print a less severe warning message here.
- Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified "
- "assertion : "
- << n << std::endl;
+ Warning()
+ << "Warning : SolverEngine::checkModel(): cannot check simplified "
+ "assertion : "
+ << n << std::endl;
noCheckList.push_back(n);
continue;
}
// Assertions that simplify to false result in an InternalError or
// Warning being thrown below (when hardFailure is false).
- Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
+ Notice() << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
<< std::endl;
std::stringstream ss;
- ss << "SmtEngine::checkModel(): "
+ ss << "SolverEngine::checkModel(): "
<< "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl
<< "assertion: " << assertion << std::endl
<< "simplifies to: " << n << std::endl
}
if (noCheckList.empty())
{
- Notice() << "SmtEngine::checkModel(): all assertions checked out OK !"
+ Notice() << "SolverEngine::checkModel(): all assertions checked out OK !"
<< std::endl;
return;
}
* directory for licensing information.
* ****************************************************************************
*
- * The dump manager of the SmtEngine.
+ * The dump manager of the SolverEngine.
*/
#include "cvc5_private.h"
DumpManager(context::UserContext* u);
~DumpManager();
/**
- * Finish init, called during SmtEngine::finishInit, which is triggered
+ * Finish init, called during SolverEngine::finishInit, which is triggered
* when initialization of options is finished.
*/
void finishInit();
/**
- * Reset assertions, called on SmtEngine::resetAssertions.
+ * Reset assertions, called on SolverEngine::resetAssertions.
*/
void resetAssertions();
/**
bool d_fullyInited;
/**
* A vector of declaration commands waiting to be dumped out.
- * Once the SmtEngine is fully initialized, we'll dump them.
+ * Once the SolverEngine is fully initialized, we'll dump them.
* This ensures the declarations come after the set-logic and
* any necessary set-option commands are dumped.
*/
/**
* The environment class.
*
- * This class lives in the SmtEngine and contains all utilities that are
+ * This class lives in the SolverEngine and contains all utilities that are
* globally available to all internal code.
*/
class Env
{
- friend class SmtEngine;
+ friend class SolverEngine;
friend class smt::PfManager;
public:
/**
* Get the underlying proof node manager. Note since proofs depend on option
- * initialization, this is only available after the SmtEngine that owns this
- * environment is initialized, and only non-null if proofs are enabled.
+ * initialization, this is only available after the SolverEngine that owns
+ * this environment is initialized, and only non-null if proofs are enabled.
*/
ProofNodeManager* getProofNodeManager();
std::unique_ptr<context::UserContext> d_userContext;
/**
* A pointer to the node manager of this environment. A node manager is
- * not necessarily unique to an SmtEngine instance.
+ * not necessarily unique to an SolverEngine instance.
*/
NodeManager* d_nodeManager;
/**
* A pointer to the proof node manager, which is non-null if proofs are
- * enabled. This is owned by the proof manager of the SmtEngine that owns
+ * enabled. This is owned by the proof manager of the SolverEngine that owns
* this environment.
*/
ProofNodeManager* d_proofNodeManager;
* The rewriter owned by this Env. We have a different instance
* of the rewriter for each Env instance. This is because rewriters may
* hold references to objects that belong to theory solvers, which are
- * specific to an SmtEngine/TheoryEngine instance.
+ * specific to an SolverEngine/TheoryEngine instance.
*/
std::unique_ptr<theory::Rewriter> d_rewriter;
/** Evaluator that also invokes the rewriter */
std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
/**
* The options object, which contains the modified version of the options
- * provided as input to the SmtEngine that owns this environment. Note
+ * provided as input to the SolverEngine that owns this environment. Note
* that d_options may be modified by the options manager, e.g. based
* on the input logic.
*
"Cannot get interpolation when produce-interpol options is off.";
throw ModalException(msg);
}
- Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj
+ Trace("sygus-interpol") << "SolverEngine::getInterpol: conjecture " << conj
<< std::endl;
// must expand definitions
Node conjn = d_env.getTopLevelSubstitutions().apply(conj);
const Node& conj)
{
Assert(interpol.getType().isBoolean());
- Trace("check-interpol") << "SmtEngine::checkInterpol: get expanded assertions"
- << std::endl;
+ Trace("check-interpol")
+ << "SolverEngine::checkInterpol: get expanded assertions" << std::endl;
// two checks: first, axioms imply interpol, second, interpol implies conj.
for (unsigned j = 0; j < 2; j++)
if (j == 1)
{
Trace("check-interpol")
- << "SmtEngine::checkInterpol: conjecture is " << conj << std::endl;
+ << "SolverEngine::checkInterpol: conjecture is " << conj << std::endl;
}
- Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+ Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
<< ": make new SMT engine" << std::endl;
// Start new SMT engine to check solution
- std::unique_ptr<SmtEngine> itpChecker;
+ std::unique_ptr<SolverEngine> itpChecker;
initializeSubsolver(itpChecker, d_env);
- Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+ Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
<< ": asserting formulas" << std::endl;
if (j == 0)
{
Assert(!conj.isNull());
itpChecker->assertFormula(conj.notNode());
}
- Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+ Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
<< ": check the assertions" << std::endl;
Result r = itpChecker->checkSat();
- Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+ Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
<< ": result is " << r << std::endl;
std::stringstream serr;
if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
{
if (j == 0)
{
- serr << "SmtEngine::checkInterpol(): negated produced solution cannot "
+ serr << "SolverEngine::checkInterpol(): negated produced solution "
+ "cannot "
"be shown "
"satisfiable with assertions, result was "
<< r;
}
else
{
- serr
- << "SmtEngine::checkInterpol(): negated conjecture cannot be shown "
- "satisfiable with produced solution, result was "
- << r;
+ serr << "SolverEngine::checkInterpol(): negated conjecture cannot be "
+ "shown "
+ "satisfiable with produced solution, result was "
+ << r;
}
InternalError() << serr.str();
}
* A solver for interpolation queries.
*
* This class is responsible for responding to get-interpol commands. It spawns
- * a subsolver SmtEngine for a sygus conjecture that captures the interpolation
- * query, and implements supporting utility methods such as checkInterpol.
+ * a subsolver SolverEngine for a sygus conjecture that captures the
+ * interpolation query, and implements supporting utility methods such as
+ * checkInterpol.
*/
class InterpolationSolver : protected EnvObj
{
namespace cvc5 {
namespace smt {
-ResourceOutListener::ResourceOutListener(SmtEngine& smt) : d_smt(smt) {}
+ResourceOutListener::ResourceOutListener(SolverEngine& slv) : d_slv(slv) {}
void ResourceOutListener::notify()
{
- SmtScope scope(&d_smt);
+ SmtScope scope(&d_slv);
Assert(smt::smtEngineInScope());
- d_smt.interrupt();
+ d_slv.interrupt();
}
SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm,
namespace cvc5 {
class OutputManager;
-class SmtEngine;
+class SolverEngine;
namespace smt {
class ResourceOutListener : public Listener
{
public:
- ResourceOutListener(SmtEngine& smt);
- /** notify method, interupts SmtEngine */
+ ResourceOutListener(SolverEngine& smt);
+ /** notify method, interupts SolverEngine */
void notify() override;
private:
- /** Reference to the SmtEngine */
- SmtEngine& d_smt;
+ /** Reference to the SolverEngine */
+ SolverEngine& d_slv;
};
class DumpManager;
return out;
}
-OptimizationSolver::OptimizationSolver(SmtEngine* parent)
+OptimizationSolver::OptimizationSolver(SolverEngine* parent)
: d_parent(parent),
d_optChecker(),
d_objectives(parent->getUserContext()),
return d_results;
}
-std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
- SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
+std::unique_ptr<SolverEngine> OptimizationSolver::createOptCheckerWithTimeout(
+ SolverEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
{
- std::unique_ptr<SmtEngine> optChecker;
+ std::unique_ptr<SolverEngine> optChecker;
// initializeSubSolver will copy the options and theories enabled
// from the current solver to optChecker and adds timeout
theory::initializeSubsolver(
namespace cvc5 {
class Env;
-class SmtEngine;
+class SolverEngine;
namespace smt {
* A solver for optimization queries.
*
* This class is responsible for responding to optmization queries. It
- * spawns a subsolver SmtEngine that captures the parent assertions and
+ * spawns a subsolver SolverEngine that captures the parent assertions and
* implements a linear optimization loop. Supports activateObjective,
* checkOpt, and objectiveGetValue in that order.
*/
* Constructor
* @param parent the smt_solver that the user added their assertions to
**/
- OptimizationSolver(SmtEngine* parent);
+ OptimizationSolver(SolverEngine* parent);
~OptimizationSolver() = default;
/**
* @param timeout the timeout value, given in milliseconds (ms)
* @return a unique_pointer of SMT subsolver
**/
- static std::unique_ptr<SmtEngine> createOptCheckerWithTimeout(
- SmtEngine* parentSMTSolver,
+ static std::unique_ptr<SolverEngine> createOptCheckerWithTimeout(
+ SolverEngine* parentSMTSolver,
bool needsTimeout = false,
unsigned long timeout = 0);
Result optimizeParetoNaiveGIA();
/** A pointer to the parent SMT engine **/
- SmtEngine* d_parent;
+ SolverEngine* d_parent;
/** A subsolver for offline optimization **/
- std::unique_ptr<SmtEngine> d_optChecker;
+ std::unique_ptr<SolverEngine> d_optChecker;
/** The objectives to optimize for **/
context::CDList<OptimizationObjective> d_objectives;
namespace cvc5 {
-OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {}
+OutputManager::OutputManager(SolverEngine* slv) : d_slv(slv) {}
-const Printer& OutputManager::getPrinter() const { return d_smt->getPrinter(); }
+const Printer& OutputManager::getPrinter() const { return d_slv->getPrinter(); }
std::ostream& OutputManager::getDumpOut() const
{
- return *d_smt->getOptions().base.out;
+ return *d_slv->getOptions().base.out;
}
} // namespace cvc5
* directory for licensing information.
* ****************************************************************************
*
- * The output manager for the SmtEngine.
+ * The output manager for the SolverEngine.
*
* The output manager provides helper functions for printing commands
* internally.
namespace cvc5 {
class Printer;
-class SmtEngine;
+class SolverEngine;
/** This utility class provides helper functions for printing commands
* internally */
*
* @param smt SMT engine to manage output for
*/
- explicit OutputManager(SmtEngine* smt);
+ explicit OutputManager(SolverEngine* smt);
/** Get the current printer based on the current options
*
std::ostream& getDumpOut() const;
private:
- SmtEngine* d_smt;
+ SolverEngine* d_slv;
};
} // namespace cvc5
namespace cvc5 {
namespace smt {
-Preprocessor::Preprocessor(SmtEngine& smt,
+Preprocessor::Preprocessor(SolverEngine& slv,
Env& env,
AbstractValues& abs,
SmtEngineStatistics& stats)
- : d_smt(smt),
+ : d_slv(slv),
d_env(env),
d_absValues(abs),
d_propagator(true, true),
d_assertionsProcessed(env.getUserContext(), false),
d_exDefs(env, stats),
- d_processor(smt, *env.getResourceManager(), stats),
+ d_processor(slv, *env.getResourceManager(), stats),
d_pnm(nullptr)
{
}
void Preprocessor::finishInit()
{
d_ppContext.reset(new preprocessing::PreprocessingPassContext(
- &d_smt, d_env, &d_propagator));
+ &d_slv, d_env, &d_propagator));
// initialize the preprocessing passes
d_processor.finishInit(d_ppContext.get());
Trace("smt") << "SMT simplify(" << node << ")" << endl;
if (Dump.isOn("benchmark"))
{
- d_smt.getOutputManager().getPrinter().toStreamCmdSimplify(
- d_smt.getOutputManager().getDumpOut(), node);
+ d_slv.getOutputManager().getPrinter().toStreamCmdSimplify(
+ d_slv.getOutputManager().getDumpOut(), node);
}
Node ret = expandDefinitions(node);
ret = theory::Rewriter::rewrite(ret);
* directory for licensing information.
* ****************************************************************************
*
- * The preprocessor of the SmtEngine.
+ * The preprocessor of the SolverEngine.
*/
#include "cvc5_private.h"
class Preprocessor
{
public:
- Preprocessor(SmtEngine& smt,
+ Preprocessor(SolverEngine& smt,
Env& env,
AbstractValues& abs,
SmtEngineStatistics& stats);
/**
* Cleanup, which deletes the processing passes owned by this module. This
* is required to be done explicitly so that passes are deleted before the
- * objects they refer to in the SmtEngine destructor.
+ * objects they refer to in the SolverEngine destructor.
*/
void cleanup();
/**
void setProofGenerator(PreprocessProofGenerator* pppg);
private:
- /** Reference to the parent SmtEngine */
- SmtEngine& d_smt;
+ /** Reference to the parent SolverEngine */
+ SolverEngine& d_slv;
/** Reference to the env */
Env& d_env;
/** Reference to the abstract values utility */
unsigned& d_depth;
};
-ProcessAssertions::ProcessAssertions(SmtEngine& smt,
+ProcessAssertions::ProcessAssertions(SolverEngine& slv,
ResourceManager& rm,
SmtEngineStatistics& stats)
- : d_smt(smt),
+ : d_slv(slv),
d_resourceManager(rm),
d_smtStats(stats),
d_preprocessingPassContext(nullptr)
d_passes["sep-skolem-emp"]->apply(&assertions);
}
- if (d_smt.getLogicInfo().isQuantified())
+ if (d_slv.getLogicInfo().isQuantified())
{
// remove rewrite rules, apply pre-skolemization to existential quantifiers
d_passes["quantifiers-preprocess"]->apply(&assertions);
}
// rephrasing normal inputs as sygus problems
- if (!d_smt.isInternalSubsolver())
+ if (!d_slv.isInternalSubsolver())
{
if (options::sygusInference())
{
d_passes["bv-eager-atoms"]->apply(&assertions);
}
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
+ Trace("smt-proc") << "ProcessAssertions::apply() end" << endl;
dumpAssertions("post-everything", assertions);
return noConflict;
{
ScopeCounter depth(d_simplifyAssertionsDepth);
- Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
+ Trace("simplify") << "ProcessAssertions::simplify()" << endl;
if (options::simplificationMode() != options::SimplificationMode::NONE)
{
if ( // check that option is on
options::arithMLTrick() &&
// only useful in arith
- d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
+ d_slv.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
// we add new assertions and need this (in practice, this
// restriction only disables miplib processing during
// re-simplification, which we don't expect to be useful anyway)
}
else
{
- Trace("simplify") << "SmtEnginePrivate::simplify(): "
+ Trace("simplify") << "ProcessAssertions::simplify(): "
<< "skipping miplib pseudobooleans pass..." << endl;
}
}
for (unsigned i = 0; i < assertionList.size(); ++i)
{
TNode n = assertionList[i];
- d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
- d_smt.getOutputManager().getDumpOut(), n);
+ d_slv.getOutputManager().getPrinter().toStreamCmdAssert(
+ d_slv.getOutputManager().getDumpOut(), n);
}
}
}
namespace cvc5 {
-class SmtEngine;
+class SolverEngine;
namespace preprocessing {
class AssertionPipeline;
typedef std::unordered_map<Node, bool> NodeToBoolHashMap;
public:
- ProcessAssertions(SmtEngine& smt,
+ ProcessAssertions(SolverEngine& smt,
ResourceManager& rm,
SmtEngineStatistics& stats);
~ProcessAssertions();
private:
/** Reference to the SMT engine */
- SmtEngine& d_smt;
+ SolverEngine& d_slv;
/** Reference to resource manager */
ResourceManager& d_resourceManager;
/** Reference to the SMT stats */
{
// Note this assumes that setFinalProof is only called once per unsat
// response. This method would need to cache its result otherwise.
- Trace("smt-proof") << "SmtEngine::setFinalProof(): get proof body...\n";
+ Trace("smt-proof") << "SolverEngine::setFinalProof(): get proof body...\n";
if (Trace.isOn("smt-proof-debug"))
{
Trace("smt-proof-debug")
- << "SmtEngine::setFinalProof(): Proof node for false:\n";
+ << "SolverEngine::setFinalProof(): Proof node for false:\n";
Trace("smt-proof-debug") << *pfn.get() << std::endl;
Trace("smt-proof-debug") << "=====" << std::endl;
}
if (Trace.isOn("smt-proof"))
{
- Trace("smt-proof") << "SmtEngine::setFinalProof(): get free assumptions..."
- << std::endl;
+ Trace("smt-proof")
+ << "SolverEngine::setFinalProof(): get free assumptions..."
+ << std::endl;
std::vector<Node> fassumps;
expr::getFreeAssumptions(pfn.get(), fassumps);
Trace("smt-proof")
- << "SmtEngine::setFinalProof(): initial free assumptions are:\n";
+ << "SolverEngine::setFinalProof(): initial free assumptions are:\n";
for (const Node& a : fassumps)
{
Trace("smt-proof") << "- " << a << std::endl;
}
- Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n";
+ Trace("smt-proof") << "SolverEngine::setFinalProof(): assertions are:\n";
for (const Node& n : assertions)
{
Trace("smt-proof") << "- " << n << std::endl;
Trace("smt-proof") << "=====" << std::endl;
}
- Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n";
+ Trace("smt-proof") << "SolverEngine::setFinalProof(): postprocess...\n";
Assert(d_pfpp != nullptr);
d_pfpp->process(pfn);
- Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n";
+ Trace("smt-proof") << "SolverEngine::setFinalProof(): make scope...\n";
// Now make the final scope, which ensures that the only open leaves of the
// proof are the assertions.
d_finalProof = d_pnm->mkScope(pfn, assertions);
- Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
+ Trace("smt-proof") << "SolverEngine::setFinalProof(): finished.\n";
}
void PfManager::printProof(std::ostream& out,
* directory for licensing information.
* ****************************************************************************
*
- * The proof manager of SmtEngine.
+ * The proof manager of SolverEngine.
*/
#include "cvc5_private.h"
class ProofChecker;
class ProofNode;
class ProofNodeManager;
-class SmtEngine;
+class SolverEngine;
namespace rewriter {
class RewriteDb;
class ProofPostproccess;
/**
- * This class is responsible for managing the proof output of SmtEngine, as
+ * This class is responsible for managing the proof output of SolverEngine, as
* well as setting up the global proof checker and proof node manager.
*
- * The proof production of an SmtEngine is directly impacted by whether, and
+ * The proof production of an SolverEngine is directly impacted by whether, and
* how, we are producing unsat cores:
*
* - If we are producing unsat cores using the old proof infrastructure, then
- * SmtEngine will not have proofs in the sense of this proof manager.
+ * SolverEngine will not have proofs in the sense of this proof manager.
*
* - If we are producing unsat cores using this proof infrastructure, then the
- * SmtEngine will have proofs using this proof manager, according to the unsat
- * core mode:
+ * SolverEngine will have proofs using this proof manager, according to the
+ * unsat core mode:
*
* - assumption mode: proofs only for preprocessing, not in sat solver or
* theory engine, and level of granularity set to off (unless otherwise
* Note that if --produce-proofs is set then full-proof mode of unsat cores is
* forced.
*
- * - If we are not producing unsat cores then the SmtEngine will have proofs as
- * long as --produce-proofs is on.
+ * - If we are not producing unsat cores then the SolverEngine will have proofs
+ * as long as --produce-proofs is on.
*
- * - If SmtEngine has been configured in a way that is incompatible with proofs
- * then unsat core production will be disabled.
+ * - If SolverEngine has been configured in a way that is incompatible with
+ * proofs then unsat core production will be disabled.
*/
class PfManager : protected EnvObj
{
* connected by setFinalProof().
*/
std::shared_ptr<ProofNode> d_finalProof;
-}; /* class SmtEngine */
+}; /* class SolverEngine */
} // namespace smt
} // namespace cvc5
namespace smt {
/**
- * A callback class used by SmtEngine for post-processing proof nodes by
+ * A callback class used by SolverEngine for post-processing proof nodes by
* connecting proofs of preprocessing, and expanding macro PfRule applications.
*/
class ProofPostprocessCallback : public ProofNodeUpdaterCallback
/**
* The proof postprocessor module. This postprocesses the final proof
- * produced by an SmtEngine. Its main two tasks are to:
+ * produced by an SolverEngine. Its main two tasks are to:
* (1) Connect proofs of preprocessing,
* (2) Expand macro PfRule applications.
*/
std::vector<Node> insts;
qe->getInstantiations(topq, insts);
// note we do not convert to witness form here, since we could be
- // an internal subsolver (SmtEngine::isInternalSubsolver).
+ // an internal subsolver (SolverEngine::isInternalSubsolver).
ret = nm->mkAnd(insts);
Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
if (q.getKind() == EXISTS)
* elimination is LRA and LIA.
*
* This function returns a formula ret such that, given
- * the current set of formulas A asserted to this SmtEngine :
+ * the current set of formulas A asserted to this SolverEngine :
*
* If doFull = true, then
* - ( A ^ q ) and ( A ^ ret ) are equivalent
* for incrementally computing the result of a
* quantifier elimination.
*
- * @param as The assertions of the SmtEngine
+ * @param as The assertions of the SolverEngine
* @param q The quantified formula we are eliminating quantifiers from
* @param doFull Whether we are doing full quantifier elimination on q
- * @param isInternalSubsolver Whether the SmtEngine we belong to is an
+ * @param isInternalSubsolver Whether the SolverEngine we belong to is an
* internal subsolver. If it is not, then we convert the final result to
* witness form.
* @return The result of eliminating quantifiers from q.
if (opts.bv.bitvectorAigSimplificationsWasSetByUser)
{
- Notice() << "SmtEngine: setting bitvectorAig" << std::endl;
+ Notice() << "SolverEngine: setting bitvectorAig" << std::endl;
opts.bv.bitvectorAig = true;
}
if (opts.bv.bitvectorAlgebraicBudgetWasSetByUser)
{
- Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl;
+ Notice() << "SolverEngine: setting bitvectorAlgebraicSolver" << std::endl;
opts.bv.bitvectorAlgebraicSolver = true;
}
{
opts.smt.unsatCores = false;
opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
- Notice() << "SmtEngine: turning off produce-proofs due to "
+ Notice() << "SolverEngine: turning off produce-proofs due to "
<< reasonNoProofs.str() << "." << std::endl;
opts.smt.produceProofs = false;
opts.smt.checkProofs = false;
"for the combination of bit-vectors with arrays or uinterpreted "
"functions. Try --bitblast=lazy"));
}
- Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
- << "generation" << std::endl;
+ Notice()
+ << "SolverEngine: setting bit-blast mode to lazy to support model"
+ << "generation" << std::endl;
opts.bv.bitblastMode = options::BitblastMode::LAZY;
}
else if (!opts.base.incrementalSolving)
throw OptionException(std::string(
"Ackermannization currently does not support model generation."));
}
- Notice() << "SmtEngine: turn off ackermannization to support model"
+ Notice() << "SolverEngine: turn off ackermannization to support model"
<< "generation" << std::endl;
opts.smt.ackermann = false;
}
|| opts.smt.produceProofs)
&& !opts.smt.produceAssertions)
{
- Notice() << "SmtEngine: turning on produce-assertions to support "
+ Notice() << "SolverEngine: turning on produce-assertions to support "
<< "option requiring assertions." << std::endl;
opts.smt.produceAssertions = true;
}
"bool-to-bv != off not supported with CBQI BV for quantified "
"logics");
}
- Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
- << std::endl;
+ Notice()
+ << "SolverEngine: turning off bool-to-bitvector to support CBQI BV"
+ << std::endl;
opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
}
}
&& (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck
|| usesSygus(opts)))
{
- Notice() << "SmtEngine: turning on produce-models" << std::endl;
+ Notice() << "SolverEngine: turning on produce-models" << std::endl;
opts.smt.produceModels = true;
}
throw OptionException(
"bool-to-bv=all not supported for non-bitvector logics.");
}
- Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
+ Notice() << "SolverEngine: turning off bool-to-bv for non-bv logic: "
<< logic.getLogicString() << std::endl;
opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
}
{
if (opts.theory.relevanceFilterWasSetByUser)
{
- Warning() << "SmtEngine: turning on relevance filtering to support "
+ Warning() << "SolverEngine: turning on relevance filtering to support "
"--nl-ext-rlv="
<< opts.arith.nlRlvMode << std::endl;
}
ss << "Cannot use " << sOptNoModel << " with model generation.";
throw OptionException(ss.str());
}
- Notice() << "SmtEngine: turning off produce-models to support "
+ Notice() << "SolverEngine: turning off produce-models to support "
<< sOptNoModel << std::endl;
opts.smt.produceModels = false;
}
<< " with model generation (produce-assignments).";
throw OptionException(ss.str());
}
- Notice() << "SmtEngine: turning off produce-assignments to support "
+ Notice() << "SolverEngine: turning off produce-assignments to support "
<< sOptNoModel << std::endl;
opts.smt.produceAssignments = false;
}
<< " with model generation (check-models).";
throw OptionException(ss.str());
}
- Notice() << "SmtEngine: turning off check-models to support "
+ Notice() << "SolverEngine: turning off check-models to support "
<< sOptNoModel << std::endl;
opts.smt.checkModels = false;
}
reason << "unconstrained simplification";
return true;
}
- Notice() << "SmtEngine: turning off unconstrained simplification to "
+ Notice() << "SolverEngine: turning off unconstrained simplification to "
"support incremental solving"
<< std::endl;
opts.smt.unconstrainedSimp = false;
reason << "sygus inference";
return true;
}
- Notice() << "SmtEngine: turning off sygus inference to support "
+ Notice() << "SolverEngine: turning off sygus inference to support "
"incremental solving"
<< std::endl;
opts.quantifiers.sygusInference = false;
reason << "simplification";
return true;
}
- Notice() << "SmtEngine: turning off simplification to support unsat "
+ Notice() << "SolverEngine: turning off simplification to support unsat "
"cores"
<< std::endl;
opts.smt.simplificationMode = options::SimplificationMode::NONE;
reason << "learned rewrites";
return true;
}
- Notice() << "SmtEngine: turning off learned rewrites to support "
+ Notice() << "SolverEngine: turning off learned rewrites to support "
"unsat cores\n";
opts.smt.learnedRewrite = false;
}
reason << "pseudoboolean rewrites";
return true;
}
- Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
+ Notice() << "SolverEngine: turning off pseudoboolean rewrites to support "
"unsat cores\n";
opts.arith.pbRewrites = false;
}
reason << "sort inference";
return true;
}
- Notice() << "SmtEngine: turning off sort inference to support unsat "
+ Notice() << "SolverEngine: turning off sort inference to support unsat "
"cores\n";
opts.smt.sortInference = false;
}
reason << "pre-skolemization";
return true;
}
- Notice() << "SmtEngine: turning off pre-skolemization to support "
+ Notice() << "SolverEngine: turning off pre-skolemization to support "
"unsat cores\n";
opts.quantifiers.preSkolemQuant = false;
}
reason << "bv-to-bool";
return true;
}
- Notice() << "SmtEngine: turning off bitvector-to-bool to support "
+ Notice() << "SolverEngine: turning off bitvector-to-bool to support "
"unsat cores\n";
opts.bv.bitvectorToBool = false;
}
reason << "bool-to-bv != off";
return true;
}
- Notice() << "SmtEngine: turning off bool-to-bv to support unsat cores\n";
+ Notice() << "SolverEngine: turning off bool-to-bv to support unsat cores\n";
opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
}
reason << "bv-intro-pow2";
return true;
}
- Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat cores";
+ Notice()
+ << "SolverEngine: turning off bv-intro-pow2 to support unsat cores";
opts.bv.bvIntroducePow2 = false;
}
reason << "repeat-simp";
return true;
}
- Notice() << "SmtEngine: turning off repeat-simp to support unsat cores\n";
+ Notice()
+ << "SolverEngine: turning off repeat-simp to support unsat cores\n";
opts.smt.repeatSimp = false;
}
reason << "global-negate";
return true;
}
- Notice() << "SmtEngine: turning off global-negate to support unsat "
+ Notice() << "SolverEngine: turning off global-negate to support unsat "
"cores\n";
opts.quantifiers.globalNegate = false;
}
reason << "unconstrained simplification";
return true;
}
- Notice() << "SmtEngine: turning off unconstrained simplification to "
+ Notice() << "SolverEngine: turning off unconstrained simplification to "
"support unsat cores"
<< std::endl;
opts.smt.unconstrainedSimp = false;
if (opts.quantifiers.instMaxLevel != -1)
{
- Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
+ Notice() << "SolverEngine: turning off cbqi to support instMaxLevel"
<< std::endl;
opts.quantifiers.cegqi = false;
}
public:
/**
* @param isInternalSubsolver Whether we are setting the options for an
- * internal subsolver (see SmtEngine::isInternalSubsolver).
+ * internal subsolver (see SolverEngine::isInternalSubsolver).
*/
SetDefaults(bool isInternalSubsolver);
/**
* The purpose of this method is to set the default options and update the
* logic info for an SMT engine.
*
- * @param logic A reference to the logic of SmtEngine, which can be
+ * @param logic A reference to the logic of SolverEngine, which can be
* updated by this method based on the current options and the logic itself.
* @param opts The options to modify, typically the main options of the
- * SmtEngine in scope.
+ * SolverEngine in scope.
*/
void setDefaults(LogicInfo& logic, Options& opts);
namespace cvc5 {
namespace smt {
-thread_local SmtEngine* s_smtEngine_current = NULL;
+thread_local SolverEngine* s_slvEngine_current = nullptr;
-SmtEngine* currentSmtEngine() {
- Assert(s_smtEngine_current != NULL);
- return s_smtEngine_current;
+SolverEngine* currentSolverEngine()
+{
+ Assert(s_slvEngine_current != nullptr);
+ return s_slvEngine_current;
}
-bool smtEngineInScope() { return s_smtEngine_current != NULL; }
+bool smtEngineInScope() { return s_slvEngine_current != nullptr; }
ResourceManager* currentResourceManager()
{
- return s_smtEngine_current->getResourceManager();
+ return s_slvEngine_current->getResourceManager();
}
-SmtScope::SmtScope(const SmtEngine* smt)
- : d_oldSmtEngine(s_smtEngine_current),
- d_optionsScope(smt ? &const_cast<SmtEngine*>(smt)->getOptions() : nullptr)
+SmtScope::SmtScope(const SolverEngine* smt)
+ : d_oldSlvEngine(s_slvEngine_current),
+ d_optionsScope(smt ? &const_cast<SolverEngine*>(smt)->getOptions()
+ : nullptr)
{
- Assert(smt != NULL);
- s_smtEngine_current = const_cast<SmtEngine*>(smt);
- Debug("current") << "smt scope: " << s_smtEngine_current << std::endl;
+ Assert(smt != nullptr);
+ s_slvEngine_current = const_cast<SolverEngine*>(smt);
+ Debug("current") << "smt scope: " << s_slvEngine_current << std::endl;
}
SmtScope::~SmtScope() {
- s_smtEngine_current = d_oldSmtEngine;
- Debug("current") << "smt scope: returning to " << s_smtEngine_current
+ s_slvEngine_current = d_oldSlvEngine;
+ Debug("current") << "smt scope: returning to " << s_slvEngine_current
<< std::endl;
}
StatisticsRegistry& SmtScope::currentStatisticsRegistry()
{
Assert(smtEngineInScope());
- return s_smtEngine_current->getStatisticsRegistry();
+ return s_slvEngine_current->getStatisticsRegistry();
}
} // namespace smt
namespace cvc5 {
-class SmtEngine;
+class SolverEngine;
class StatisticsRegistry;
namespace smt {
-SmtEngine* currentSmtEngine();
+SolverEngine* currentSolverEngine();
bool smtEngineInScope();
/** get the current resource manager */
class SmtScope
{
public:
- SmtScope(const SmtEngine* smt);
+ SmtScope(const SolverEngine* smt);
~SmtScope();
/**
* This returns the StatisticsRegistry attached to the currently in scope
- * SmtEngine.
+ * SolverEngine.
*/
static StatisticsRegistry& currentStatisticsRegistry();
private:
- /** The old SmtEngine, to be restored on destruction. */
- SmtEngine* d_oldSmtEngine;
+ /** The old SolverEngine, to be restored on destruction. */
+ SolverEngine* d_oldSlvEngine;
/** Options scope */
Options::OptionsScope d_optionsScope;
};/* class SmtScope */
namespace cvc5 {
namespace smt {
-SmtEngineState::SmtEngineState(Env& env, SmtEngine& smt)
- : d_smt(smt),
+SmtEngineState::SmtEngineState(Env& env, SolverEngine& slv)
+ : d_slv(slv),
d_env(env),
d_pendingPops(0),
d_fullyInited(false),
doPendingPops();
if (options::incrementalSolving())
{
- // notifies the SmtEngine to process the assertions immediately
- d_smt.notifyPushPre();
+ // notifies the SolverEngine to process the assertions immediately
+ d_slv.notifyPushPre();
getUserContext()->push();
// the context push is done inside of the SAT solver
- d_smt.notifyPushPost();
+ d_slv.notifyPushPost();
}
}
// check to see if a postsolve() is pending
if (d_needPostsolve)
{
- d_smt.notifyPostSolvePre();
+ d_slv.notifyPostSolvePre();
}
while (d_pendingPops > 0)
{
// the context pop is done inside of the SAT solver
- d_smt.notifyPopPre();
+ d_slv.notifyPopPre();
// pop the context
getUserContext()->pop();
--d_pendingPops;
}
if (d_needPostsolve)
{
- d_smt.notifyPostSolvePost();
+ d_slv.notifyPostSolvePost();
d_needPostsolve = false;
}
}
namespace cvc5 {
-class SmtEngine;
+class SolverEngine;
class Env;
namespace smt {
/**
- * This utility is responsible for maintaining the basic state of the SmtEngine.
+ * This utility is responsible for maintaining the basic state of the
+ * SolverEngine.
*
- * It has no concept of anything related to the assertions of the SmtEngine,
+ * It has no concept of anything related to the assertions of the SolverEngine,
* or more generally it does not depend on Node.
*
* This class has three sets of interfaces:
- * (1) notification methods that are used by SmtEngine to notify when an event
- * occurs (e.g. the beginning of a check-sat call),
- * (2) maintaining the SAT and user contexts to be used by the SmtEngine,
- * (3) general information queries, including the mode that the SmtEngine is
- * in, based on the notifications it has received.
+ * (1) notification methods that are used by SolverEngine to notify when an
+ * event occurs (e.g. the beginning of a check-sat call), (2) maintaining the
+ * SAT and user contexts to be used by the SolverEngine, (3) general information
+ * queries, including the mode that the SolverEngine is in, based on the
+ * notifications it has received.
*
- * It maintains a reference to the SmtEngine for the sake of making callbacks.
+ * It maintains a reference to the SolverEngine for the sake of making
+ * callbacks.
*/
class SmtEngineState
{
public:
- SmtEngineState(Env& env, SmtEngine& smt);
+ SmtEngineState(Env& env, SolverEngine& smt);
~SmtEngineState() {}
/**
* Notify that the expected status of the next check-sat is given by the
*/
void notifyExpectedStatus(const std::string& status);
/**
- * Notify that the SmtEngine is fully initialized, which is called when
+ * Notify that the SolverEngine is fully initialized, which is called when
* options are finalized.
*/
void notifyFullyInited();
* Notify that we finished an abduction query, where success is whether the
* command was successful. This is managed independently of the above
* calls for notifying check-sat. In other words, if a get-abduct command
- * is issued to an SmtEngine, it may use a satisfiability call (if desired)
+ * is issued to an SolverEngine, it may use a satisfiability call (if desired)
* to solve the abduction query. This method is called *in addition* to
* the above calls to notifyCheckSat / notifyCheckSatResult in this case.
* In particular, it is called after these two methods are completed.
* Notify that we finished an interpolation query, where success is whether
* the command was successful. This is managed independently of the above
* calls for notifying check-sat. In other words, if a get-interpol command
- * is issued to an SmtEngine, it may use a satisfiability call (if desired)
+ * is issued to an SolverEngine, it may use a satisfiability call (if desired)
* to solve the interpolation query. This method is called *in addition* to
* the above calls to notifyCheckSat / notifyCheckSatResult in this case.
* In particular, it is called after these two methods are completed.
*/
void finishInit();
/**
- * Prepare for a shutdown of the SmtEngine, which does pending pops and
+ * Prepare for a shutdown of the SolverEngine, which does pending pops and
* pops the user context to zero.
*/
void shutdown();
//---------------------------- context management
/**
* Do all pending pops, which ensures that the context levels are up-to-date.
- * This method should be called by the SmtEngine before using any of its
+ * This method should be called by the SolverEngine before using any of its
* members that rely on the context (e.g. PropEngine or TheoryEngine).
*/
void doPendingPops();
/**
- * Called when the user of SmtEngine issues a push. This corresponds to
+ * Called when the user of SolverEngine issues a push. This corresponds to
* the SMT-LIB command push.
*/
void userPush();
/**
- * Called when the user of SmtEngine issues a pop. This corresponds to
+ * Called when the user of SolverEngine issues a pop. This corresponds to
* the SMT-LIB command pop.
*/
void userPop();
//---------------------------- queries
/**
- * Return true if the SmtEngine is fully initialized (post-construction).
+ * Return true if the SolverEngine is fully initialized (post-construction).
* This post-construction initialization is automatically triggered by the
- * use of the SmtEngine; e.g. when the first formula is asserted, a call
+ * use of the SolverEngine; e.g. when the first formula is asserted, a call
* to simplify() is issued, a scope is pushed, etc.
*/
bool isFullyInited() const;
/**
- * Return true if the SmtEngine is fully initialized and there are no
+ * Return true if the SolverEngine is fully initialized and there are no
* pending pops.
*/
bool isFullyReady() const;
/**
* Return true if a notifyCheckSat call has been made, e.g. a query has been
- * issued to the SmtEngine.
+ * issued to the SolverEngine.
*/
bool isQueryMade() const;
/** Return the user context level. */
* counter and does nothing.
*/
void internalPop(bool immediate = false);
- /** Reference to the SmtEngine */
- SmtEngine& d_smt;
- /** Reference to the env of the parent SmtEngine */
+ /** Reference to the SolverEngine */
+ SolverEngine& d_slv;
+ /** Reference to the env of the parent SolverEngine */
Env& d_env;
/** The context levels of user pushes */
std::vector<int> d_userLevels;
unsigned d_pendingPops;
/**
- * Whether or not the SmtEngine is fully initialized (post-construction).
+ * Whether or not the SolverEngine is fully initialized (post-construction).
* This post-construction initialization is automatically triggered by the
- * use of the SmtEngine which calls the finishInit method above; e.g. when
+ * use of the SolverEngine which calls the finishInit method above; e.g. when
* the first formula is asserted, a call to simplify() is issued, a scope is
* pushed, etc.
*/
/**
* Whether or not a notifyCheckSat call has been made, which corresponds to
* when a checkEntailed() or checkSatisfiability() has already been
- * made through the SmtEngine. If true, and incrementalSolving is false,
+ * made through the SolverEngine. If true, and incrementalSolving is false,
* then attempting an additional checks for satisfiability will fail with
* a ModalException during notifyCheckSat.
*/
/**
* Internal status flag to indicate whether we have been issued a
* notifyCheckSat call and have yet to process the "postsolve" methods of
- * SmtEngine via SmtEngine::notifyPostSolvePre/notifyPostSolvePost.
+ * SolverEngine via SolverEngine::notifyPostSolvePre/notifyPostSolvePost.
*/
bool d_needPostsolve;
/**
* Most recent result of last checkSatisfiability/checkEntailed in the
- * SmtEngine.
+ * SolverEngine.
*/
Result d_status;
struct SmtEngineStatistics
{
- SmtEngineStatistics(const std::string& name = "smt::SmtEngine::");
+ SmtEngineStatistics(const std::string& name = "smt::SolverEngine::");
/** time spent in definition-expansion */
TimerStat d_definitionExpansionTime;
/** number of constant propagations found during nonclausal simp */
* directory for licensing information.
* ****************************************************************************
*
- * Enumeration type for the mode of an SmtEngine.
+ * Enumeration type for the mode of an SolverEngine.
*/
#include "smt/smt_mode.h"
* directory for licensing information.
* ****************************************************************************
*
- * Enumeration type for the mode of an SmtEngine.
+ * Enumeration type for the mode of an SolverEngine.
*/
#include "cvc5_public.h"
* directory for licensing information.
* ****************************************************************************
*
- * The solver for SMT queries in an SmtEngine.
+ * The solver for SMT queries in an SolverEngine.
*/
#include "smt/smt_solver.h"
* directory for licensing information.
* ****************************************************************************
*
- * The solver for SMT queries in an SmtEngine.
+ * The solver for SMT queries in an SolverEngine.
*/
#include "cvc5_private.h"
namespace cvc5 {
-class SmtEngine;
+class SolverEngine;
class Env;
class TheoryEngine;
class ResourceManager;
*/
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.
+ * This is called by the destructor of SolverEngine, 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
+ * in SolverEngine. 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
+ * @param as The object managing the assertions in SolverEngine. 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.
private:
/** Reference to the environment */
Env& d_env;
- /** Reference to the state of the SmtEngine */
+ /** Reference to the state of the SolverEngine */
SmtEngineState& d_state;
- /** Reference to the preprocessor of SmtEngine */
+ /** Reference to the preprocessor of SolverEngine */
Preprocessor& d_pp;
- /** Reference to the statistics of SmtEngine */
+ /** Reference to the statistics of SolverEngine */
SmtEngineStatistics& d_stats;
/** The theory engine */
std::unique_ptr<TheoryEngine> d_theoryEngine;
* directory for licensing information.
* ****************************************************************************
*
- * Accessor for the SmtEngine's StatisticsRegistry.
+ * Accessor for the SolverEngine's StatisticsRegistry.
*/
#include "smt/smt_statistics_registry.h"
* directory for licensing information.
* ****************************************************************************
*
- * Accessor for the SmtEngine's StatisticsRegistry.
+ * Accessor for the SolverEngine's StatisticsRegistry.
*/
#include "cvc5_private.h"
/**
* This returns the StatisticsRegistry attached to the currently in scope
- * SmtEngine. This is a synonym for smt::SmtScope::currentStatisticsRegistry().
+ * SolverEngine. This is a synonym for
+ * smt::SmtScope::currentStatisticsRegistry().
*/
StatisticsRegistry& smtStatisticsRegistry();
namespace cvc5 {
-SmtEngine::SmtEngine(NodeManager* nm, const Options* optr)
+SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
: d_env(new Env(nm, optr)),
d_state(new SmtEngineState(*d_env.get(), *this)),
d_absValues(new AbstractValues(getNodeManager())),
d_pp(nullptr),
d_scope(nullptr)
{
- // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
- // we are constructing the current SmtEngine in scope for the lifetime of
- // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine
- // is then in scope during its lifetime). This is mostly to ensure that
- // options are always in scope, for e.g. printing expressions, which rely
- // on knowing the output language.
- // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally.
- // These are created, used, and deleted in a modular fashion while not
- // interleaving calls to the master SmtEngine. Thus the hack here does not
- // break this use case.
- // On the other hand, this hack breaks use cases where multiple SmtEngine
- // objects are created by the user.
+ // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SolverEngine
+ // we are constructing the current SolverEngine in scope for the lifetime of
+ // this SolverEngine, or until another SolverEngine is constructed (that
+ // SolverEngine is then in scope during its lifetime). This is mostly to
+ // ensure that options are always in scope, for e.g. printing expressions,
+ // which rely on knowing the output language. Notice that the SolverEngine may
+ // spawn new SolverEngine "subsolvers" internally. These are created, used,
+ // and deleted in a modular fashion while not interleaving calls to the master
+ // SolverEngine. Thus the hack here does not break this use case. On the other
+ // hand, this hack breaks use cases where multiple SolverEngine objects are
+ // created by the user.
d_scope.reset(new SmtScope(this));
// listen to node manager events
getNodeManager()->subscribeEvents(d_snmListener.get());
d_quantElimSolver.reset(new QuantElimSolver(*d_env.get(), *d_smtSolver));
}
-bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); }
-bool SmtEngine::isQueryMade() const { return d_state->isQueryMade(); }
-size_t SmtEngine::getNumUserLevels() const
+bool SolverEngine::isFullyInited() const { return d_state->isFullyInited(); }
+bool SolverEngine::isQueryMade() const { return d_state->isQueryMade(); }
+size_t SolverEngine::getNumUserLevels() const
{
return d_state->getNumUserLevels();
}
-SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); }
-bool SmtEngine::isSmtModeSat() const
+SmtMode SolverEngine::getSmtMode() const { return d_state->getMode(); }
+bool SolverEngine::isSmtModeSat() const
{
SmtMode mode = getSmtMode();
return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN;
}
-Result SmtEngine::getStatusOfLastCommand() const
+Result SolverEngine::getStatusOfLastCommand() const
{
return d_state->getStatus();
}
-context::UserContext* SmtEngine::getUserContext()
+context::UserContext* SolverEngine::getUserContext()
{
return d_env->getUserContext();
}
-context::Context* SmtEngine::getContext() { return d_env->getContext(); }
+context::Context* SolverEngine::getContext() { return d_env->getContext(); }
-TheoryEngine* SmtEngine::getTheoryEngine()
+TheoryEngine* SolverEngine::getTheoryEngine()
{
return d_smtSolver->getTheoryEngine();
}
-prop::PropEngine* SmtEngine::getPropEngine()
+prop::PropEngine* SolverEngine::getPropEngine()
{
return d_smtSolver->getPropEngine();
}
-void SmtEngine::finishInit()
+void SolverEngine::finishInit()
{
if (d_state->isFullyInited())
{
d_pp->setProofGenerator(pppg);
}
- Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
+ Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
d_smtSolver->finishInit(logic);
// now can construct the SMT-level model object
d_pp->finishInit();
AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
- << "The PropEngine has pushed but the SmtEngine "
+ << "The PropEngine has pushed but the SolverEngine "
"hasn't finished initializing!";
Assert(getLogicInfo().isLocked());
// store that we are finished initializing
d_state->finishInit();
- Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
+ Trace("smt-debug") << "SolverEngine::finishInit done" << std::endl;
}
-void SmtEngine::shutdown()
+void SolverEngine::shutdown()
{
d_state->shutdown();
d_env->shutdown();
}
-SmtEngine::~SmtEngine()
+SolverEngine::~SolverEngine()
{
SmtScope smts(this);
}
}
-void SmtEngine::setLogic(const LogicInfo& logic)
+void SolverEngine::setLogic(const LogicInfo& logic)
{
SmtScope smts(this);
if (d_state->isFullyInited())
{
throw ModalException(
- "Cannot set logic in SmtEngine after the engine has "
+ "Cannot set logic in SolverEngine after the engine has "
"finished initializing.");
}
d_env->d_logic = logic;
setLogicInternal();
}
-void SmtEngine::setLogic(const std::string& s)
+void SolverEngine::setLogic(const std::string& s)
{
SmtScope smts(this);
try
}
}
-void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
+void SolverEngine::setLogic(const char* logic) { setLogic(string(logic)); }
-const LogicInfo& SmtEngine::getLogicInfo() const
+const LogicInfo& SolverEngine::getLogicInfo() const
{
return d_env->getLogicInfo();
}
-LogicInfo SmtEngine::getUserLogicInfo() const
+LogicInfo SolverEngine::getUserLogicInfo() const
{
// Lock the logic to make sure that this logic can be queried. We create a
// copy of the user logic here to keep this method const.
return res;
}
-void SmtEngine::setLogicInternal()
+void SolverEngine::setLogicInternal()
{
Assert(!d_state->isFullyInited())
- << "setting logic in SmtEngine but the engine has already"
+ << "setting logic in SolverEngine but the engine has already"
" finished initializing for this run";
d_env->d_logic.lock();
d_userLogic.lock();
}
-void SmtEngine::setInfo(const std::string& key, const std::string& value)
+void SolverEngine::setInfo(const std::string& key, const std::string& value)
{
SmtScope smts(this);
}
}
-bool SmtEngine::isValidGetInfoFlag(const std::string& key) const
+bool SolverEngine::isValidGetInfoFlag(const std::string& key) const
{
if (key == "all-statistics" || key == "error-behavior" || key == "name"
|| key == "version" || key == "authors" || key == "status"
return false;
}
-std::string SmtEngine::getInfo(const std::string& key) const
+std::string SolverEngine::getInfo(const std::string& key) const
{
SmtScope smts(this);
return toSExpr(res);
}
-void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
+void SolverEngine::debugCheckFormals(const std::vector<Node>& formals,
+ Node func)
{
for (std::vector<Node>::const_iterator i = formals.begin();
i != formals.end();
}
}
-void SmtEngine::debugCheckFunctionBody(Node formula,
- const std::vector<Node>& formals,
- Node func)
+void SolverEngine::debugCheckFunctionBody(Node formula,
+ const std::vector<Node>& formals,
+ Node func)
{
TypeNode formulaType = formula.getType(d_env->getOptions().expr.typeChecking);
TypeNode funcType = func.getType();
// We distinguish here between definitions of constants and functions,
// because the type checking for them is subtly different. Perhaps we
- // should instead have SmtEngine::defineFunction() and
- // SmtEngine::defineConstant() for better clarity, although then that
+ // should instead have SolverEngine::defineFunction() and
+ // SolverEngine::defineConstant() for better clarity, although then that
// doesn't match the SMT-LIBv2 standard...
if (formals.size() > 0)
{
}
}
-void SmtEngine::defineFunction(Node func,
- const std::vector<Node>& formals,
- Node formula,
- bool global)
+void SolverEngine::defineFunction(Node func,
+ const std::vector<Node>& formals,
+ Node formula,
+ bool global)
{
SmtScope smts(this);
finishInit();
d_asserts->addDefineFunDefinition(feq, global);
}
-void SmtEngine::defineFunctionsRec(
+void SolverEngine::defineFunctionsRec(
const std::vector<Node>& funcs,
const std::vector<std::vector<Node>>& formals,
const std::vector<Node>& formulas,
}
// Assert the quantified formula. Notice we don't call assertFormula
// directly, since we should call a private member method since we have
- // already ensuring this SmtEngine is initialized above.
+ // already ensuring this SolverEngine is initialized above.
// add define recursive definition to the assertions
d_asserts->addDefineFunDefinition(lem, global);
}
}
-void SmtEngine::defineFunctionRec(Node func,
- const std::vector<Node>& formals,
- Node formula,
- bool global)
+void SolverEngine::defineFunctionRec(Node func,
+ const std::vector<Node>& formals,
+ Node formula,
+ bool global)
{
std::vector<Node> funcs;
funcs.push_back(func);
defineFunctionsRec(funcs, formals_multi, formulas, global);
}
-Result SmtEngine::quickCheck()
+Result SolverEngine::quickCheck()
{
Assert(d_state->isFullyInited());
Trace("smt") << "SMT quickCheck()" << endl;
Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
}
-TheoryModel* SmtEngine::getAvailableModel(const char* c) const
+TheoryModel* SolverEngine::getAvailableModel(const char* c) const
{
if (!d_env->getOptions().theory.assignFunctionValues)
{
return m;
}
-QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const
+QuantifiersEngine* SolverEngine::getAvailableQuantifiersEngine(
+ const char* c) const
{
QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine();
if (qe == nullptr)
return qe;
}
-void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); }
+void SolverEngine::notifyPushPre()
+{
+ d_smtSolver->processAssertions(*d_asserts);
+}
-void SmtEngine::notifyPushPost()
+void SolverEngine::notifyPushPost()
{
TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
Assert(getPropEngine() != nullptr);
getPropEngine()->push();
}
-void SmtEngine::notifyPopPre()
+void SolverEngine::notifyPopPre()
{
TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
PropEngine* pe = getPropEngine();
pe->pop();
}
-void SmtEngine::notifyPostSolvePre()
+void SolverEngine::notifyPostSolvePre()
{
PropEngine* pe = getPropEngine();
Assert(pe != nullptr);
pe->resetTrail();
}
-void SmtEngine::notifyPostSolvePost()
+void SolverEngine::notifyPostSolvePost()
{
TheoryEngine* te = getTheoryEngine();
Assert(te != nullptr);
te->postsolve();
}
-Result SmtEngine::checkSat()
+Result SolverEngine::checkSat()
{
Node nullNode;
return checkSat(nullNode);
}
-Result SmtEngine::checkSat(const Node& assumption)
+Result SolverEngine::checkSat(const Node& assumption)
{
if (Dump.isOn("benchmark"))
{
return checkSatInternal(assump, false);
}
-Result SmtEngine::checkSat(const std::vector<Node>& assumptions)
+Result SolverEngine::checkSat(const std::vector<Node>& assumptions)
{
if (Dump.isOn("benchmark"))
{
return checkSatInternal(assumptions, false);
}
-Result SmtEngine::checkEntailed(const Node& node)
+Result SolverEngine::checkEntailed(const Node& node)
{
if (Dump.isOn("benchmark"))
{
.asEntailmentResult();
}
-Result SmtEngine::checkEntailed(const std::vector<Node>& nodes)
+Result SolverEngine::checkEntailed(const std::vector<Node>& nodes)
{
return checkSatInternal(nodes, true).asEntailmentResult();
}
-Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
- bool isEntailmentCheck)
+Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
+ bool isEntailmentCheck)
{
try
{
SmtScope smts(this);
finishInit();
- Trace("smt") << "SmtEngine::"
+ Trace("smt") << "SolverEngine::"
<< (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
<< assumptions << ")" << endl;
// check the satisfiability with the solver object
Result r = d_smtSolver->checkSatisfiability(
*d_asserts.get(), assumptions, isEntailmentCheck);
- Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
- << "(" << assumptions << ") => " << r << endl;
+ Trace("smt") << "SolverEngine::"
+ << (isEntailmentCheck ? "query" : "checkSat") << "("
+ << assumptions << ") => " << r << endl;
// Check that SAT results generate a model correctly.
if (d_env->getOptions().smt.checkModels)
}
}
-std::vector<Node> SmtEngine::getUnsatAssumptions(void)
+std::vector<Node> SolverEngine::getUnsatAssumptions(void)
{
Trace("smt") << "SMT getUnsatAssumptions()" << endl;
SmtScope smts(this);
return res;
}
-Result SmtEngine::assertFormula(const Node& formula)
+Result SolverEngine::assertFormula(const Node& formula)
{
SmtScope smts(this);
finishInit();
d_state->doPendingPops();
- Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
+ Trace("smt") << "SolverEngine::assertFormula(" << formula << ")" << endl;
// Substitute out any abstract values in ex
Node n = d_absValues->substituteAbstractValues(formula);
d_asserts->assertFormula(n);
return quickCheck().asEntailmentResult();
-} /* SmtEngine::assertFormula() */
+} /* SolverEngine::assertFormula() */
/*
--------------------------------------------------------------------------
--------------------------------------------------------------------------
*/
-void SmtEngine::declareSygusVar(Node var)
+void SolverEngine::declareSygusVar(Node var)
{
SmtScope smts(this);
d_sygusSolver->declareSygusVar(var);
}
-void SmtEngine::declareSynthFun(Node func,
- TypeNode sygusType,
- bool isInv,
- const std::vector<Node>& vars)
+void SolverEngine::declareSynthFun(Node func,
+ TypeNode sygusType,
+ bool isInv,
+ const std::vector<Node>& vars)
{
SmtScope smts(this);
finishInit();
d_state->doPendingPops();
d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars);
}
-void SmtEngine::declareSynthFun(Node func,
- bool isInv,
- const std::vector<Node>& vars)
+void SolverEngine::declareSynthFun(Node func,
+ bool isInv,
+ const std::vector<Node>& vars)
{
// use a null sygus type
TypeNode sygusType;
declareSynthFun(func, sygusType, isInv, vars);
}
-void SmtEngine::assertSygusConstraint(Node n, bool isAssume)
+void SolverEngine::assertSygusConstraint(Node n, bool isAssume)
{
SmtScope smts(this);
finishInit();
d_sygusSolver->assertSygusConstraint(n, isAssume);
}
-void SmtEngine::assertSygusInvConstraint(Node inv,
- Node pre,
- Node trans,
- Node post)
+void SolverEngine::assertSygusInvConstraint(Node inv,
+ Node pre,
+ Node trans,
+ Node post)
{
SmtScope smts(this);
finishInit();
d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
}
-Result SmtEngine::checkSynth()
+Result SolverEngine::checkSynth()
{
SmtScope smts(this);
finishInit();
--------------------------------------------------------------------------
*/
-void SmtEngine::declarePool(const Node& p, const std::vector<Node>& initValue)
+void SolverEngine::declarePool(const Node& p,
+ const std::vector<Node>& initValue)
{
Assert(p.isVar() && p.getType().isSet());
finishInit();
qe->declarePool(p, initValue);
}
-Node SmtEngine::simplify(const Node& ex)
+Node SolverEngine::simplify(const Node& ex)
{
SmtScope smts(this);
finishInit();
return d_pp->simplify(ex);
}
-Node SmtEngine::expandDefinitions(const Node& ex)
+Node SolverEngine::expandDefinitions(const Node& ex)
{
getResourceManager()->spendResource(Resource::PreprocessStep);
SmtScope smts(this);
}
// TODO(#1108): Simplify the error reporting of this method.
-Node SmtEngine::getValue(const Node& ex) const
+Node SolverEngine::getValue(const Node& ex) const
{
SmtScope smts(this);
return resultNode;
}
-std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) const
+std::vector<Node> SolverEngine::getValues(const std::vector<Node>& exprs) const
{
std::vector<Node> result;
for (const Node& e : exprs)
return result;
}
-std::vector<Node> SmtEngine::getModelDomainElements(TypeNode tn) const
+std::vector<Node> SolverEngine::getModelDomainElements(TypeNode tn) const
{
Assert(tn.isSort());
TheoryModel* m = getAvailableModel("getModelDomainElements");
return m->getDomainElements(tn);
}
-bool SmtEngine::isModelCoreSymbol(Node n)
+bool SolverEngine::isModelCoreSymbol(Node n)
{
SmtScope smts(this);
Assert(n.isVar());
return tm->isModelCoreSymbol(n);
}
-std::string SmtEngine::getModel(const std::vector<TypeNode>& declaredSorts,
- const std::vector<Node>& declaredFuns)
+std::string SolverEngine::getModel(const std::vector<TypeNode>& declaredSorts,
+ const std::vector<Node>& declaredFuns)
{
SmtScope smts(this);
// !!! Note that all methods called here should have a version at the API
return ssm.str();
}
-Result SmtEngine::blockModel()
+Result SolverEngine::blockModel()
{
Trace("smt") << "SMT blockModel()" << endl;
SmtScope smts(this);
return assertFormula(eblocker);
}
-Result SmtEngine::blockModelValues(const std::vector<Node>& exprs)
+Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
{
Trace("smt") << "SMT blockModelValues()" << endl;
SmtScope smts(this);
return assertFormula(eblocker);
}
-std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
+std::pair<Node, Node> SolverEngine::getSepHeapAndNilExpr(void)
{
if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
{
return std::make_pair(heap, nil);
}
-std::vector<Node> SmtEngine::getAssertionsInternal()
+std::vector<Node> SolverEngine::getAssertionsInternal()
{
Assert(d_state->isFullyInited());
context::CDList<Node>* al = d_asserts->getAssertionList();
return res;
}
-std::vector<Node> SmtEngine::getExpandedAssertions()
+std::vector<Node> SolverEngine::getExpandedAssertions()
{
std::vector<Node> easserts = getAssertions();
// must expand definitions
d_pp->expandDefinitions(easserts);
return easserts;
}
-Env& SmtEngine::getEnv() { return *d_env.get(); }
+Env& SolverEngine::getEnv() { return *d_env.get(); }
-void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
+void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
{
if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
{
te->declareSepHeap(locT, dataT);
}
-bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
+bool SolverEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
{
SmtScope smts(this);
finishInit();
return te->getSepHeapTypes(locT, dataT);
}
-Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
+Node SolverEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
-Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
+Node SolverEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
-void SmtEngine::checkProof()
+void SolverEngine::checkProof()
{
Assert(d_env->getOptions().smt.produceProofs);
// internal check the proof
}
}
-StatisticsRegistry& SmtEngine::getStatisticsRegistry()
+StatisticsRegistry& SolverEngine::getStatisticsRegistry()
{
return d_env->getStatisticsRegistry();
}
-UnsatCore SmtEngine::getUnsatCoreInternal()
+UnsatCore SolverEngine::getUnsatCoreInternal()
{
if (!d_env->getOptions().smt.unsatCores)
{
return UnsatCore(core);
}
-std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
+std::vector<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& core)
{
Assert(options::unsatCores())
<< "cannot reduce unsat core if unsat cores are turned off";
- Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl;
+ Notice() << "SolverEngine::reduceUnsatCore(): reducing unsat core" << endl;
std::unordered_set<Node> removed;
for (const Node& skip : core)
{
- std::unique_ptr<SmtEngine> coreChecker;
+ std::unique_ptr<SolverEngine> coreChecker;
initializeSubsolver(coreChecker, *d_env.get());
coreChecker->setLogic(getLogicInfo());
coreChecker->getOptions().smt.checkUnsatCores = false;
}
else if (r.asSatisfiabilityResult().isUnknown())
{
- Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core "
- "due to "
- "unknown result.";
+ Warning()
+ << "SolverEngine::reduceUnsatCore(): could not reduce unsat core "
+ "due to "
+ "unknown result.";
}
}
}
}
-void SmtEngine::checkUnsatCore()
+void SolverEngine::checkUnsatCore()
{
Assert(d_env->getOptions().smt.unsatCores)
<< "cannot check unsat core if unsat cores are turned off";
- Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
+ Notice() << "SolverEngine::checkUnsatCore(): generating unsat core" << endl;
UnsatCore core = getUnsatCore();
// initialize the core checker
- std::unique_ptr<SmtEngine> coreChecker;
+ std::unique_ptr<SolverEngine> coreChecker;
initializeSubsolver(coreChecker, *d_env.get());
coreChecker->getOptions().smt.checkUnsatCores = false;
// disable all proof options
coreChecker->declareSepHeap(sepLocType, sepDataType);
}
- Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions"
+ Notice() << "SolverEngine::checkUnsatCore(): pushing core assertions"
<< std::endl;
theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions();
for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i)
{
Node assertionAfterExpansion = tls.apply(*i, false);
- Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
+ Notice() << "SolverEngine::checkUnsatCore(): pushing core member " << *i
<< ", expanded to " << assertionAfterExpansion << "\n";
coreChecker->assertFormula(assertionAfterExpansion);
}
{
throw;
}
- Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
+ Notice() << "SolverEngine::checkUnsatCore(): result is " << r << endl;
if (r.asSatisfiabilityResult().isUnknown())
{
- Warning()
- << "SmtEngine::checkUnsatCore(): could not check core result unknown."
- << std::endl;
+ Warning() << "SolverEngine::checkUnsatCore(): could not check core result "
+ "unknown."
+ << std::endl;
}
else if (r.asSatisfiabilityResult().isSat())
{
InternalError()
- << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
+ << "SolverEngine::checkUnsatCore(): produced core was satisfiable.";
}
}
-void SmtEngine::checkModel(bool hardFailure)
+void SolverEngine::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(al != nullptr)
- << "don't have an assertion list to check in SmtEngine::checkModel()";
+ << "don't have an assertion list to check in SolverEngine::checkModel()";
TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
- Notice() << "SmtEngine::checkModel(): generating model" << endl;
+ Notice() << "SolverEngine::checkModel(): generating model" << endl;
TheoryModel* m = getAvailableModel("check model");
Assert(m != nullptr);
d_checkModels->checkModel(m, al, hardFailure);
}
-UnsatCore SmtEngine::getUnsatCore()
+UnsatCore SolverEngine::getUnsatCore()
{
Trace("smt") << "SMT getUnsatCore()" << std::endl;
SmtScope smts(this);
return getUnsatCoreInternal();
}
-void SmtEngine::getRelevantInstantiationTermVectors(
+void SolverEngine::getRelevantInstantiationTermVectors(
std::map<Node, InstantiationList>& insts, bool getDebugInfo)
{
Assert(d_state->getMode() == SmtMode::UNSAT);
d_ucManager->getRelevantInstantiations(pfn, insts, getDebugInfo);
}
-std::string SmtEngine::getProof()
+std::string SolverEngine::getProof()
{
Trace("smt") << "SMT getProof()\n";
SmtScope smts(this);
return ss.str();
}
-void SmtEngine::printInstantiations(std::ostream& out)
+void SolverEngine::printInstantiations(std::ostream& out)
{
SmtScope smts(this);
finishInit();
}
}
-void SmtEngine::getInstantiationTermVectors(
+void SolverEngine::getInstantiationTermVectors(
std::map<Node, std::vector<std::vector<Node>>>& insts)
{
SmtScope smts(this);
qe->getInstantiationTermVectors(insts);
}
-bool SmtEngine::getSynthSolutions(std::map<Node, Node>& solMap)
+bool SolverEngine::getSynthSolutions(std::map<Node, Node>& solMap)
{
SmtScope smts(this);
finishInit();
return d_sygusSolver->getSynthSolutions(solMap);
}
-Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
+Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
{
SmtScope smts(this);
finishInit();
*d_asserts, q, doFull, d_isInternalSubsolver);
}
-bool SmtEngine::getInterpol(const Node& conj,
- const TypeNode& grammarType,
- Node& interpol)
+bool SolverEngine::getInterpol(const Node& conj,
+ const TypeNode& grammarType,
+ Node& interpol)
{
SmtScope smts(this);
finishInit();
return success;
}
-bool SmtEngine::getInterpol(const Node& conj, Node& interpol)
+bool SolverEngine::getInterpol(const Node& conj, Node& interpol)
{
TypeNode grammarType;
return getInterpol(conj, grammarType, interpol);
}
-bool SmtEngine::getAbduct(const Node& conj,
- const TypeNode& grammarType,
- Node& abd)
+bool SolverEngine::getAbduct(const Node& conj,
+ const TypeNode& grammarType,
+ Node& abd)
{
SmtScope smts(this);
finishInit();
return success;
}
-bool SmtEngine::getAbduct(const Node& conj, Node& abd)
+bool SolverEngine::getAbduct(const Node& conj, Node& abd)
{
TypeNode grammarType;
return getAbduct(conj, grammarType, abd);
}
-void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
{
SmtScope smts(this);
QuantifiersEngine* qe =
qe->getInstantiatedQuantifiedFormulas(qs);
}
-void SmtEngine::getInstantiationTermVectors(
+void SolverEngine::getInstantiationTermVectors(
Node q, std::vector<std::vector<Node>>& tvecs)
{
SmtScope smts(this);
qe->getInstantiationTermVectors(q, tvecs);
}
-std::vector<Node> SmtEngine::getAssertions()
+std::vector<Node> SolverEngine::getAssertions()
{
SmtScope smts(this);
finishInit();
return getAssertionsInternal();
}
-void SmtEngine::getDifficultyMap(std::map<Node, Node>& dmap)
+void SolverEngine::getDifficultyMap(std::map<Node, Node>& dmap)
{
Trace("smt") << "SMT getDifficultyMap()\n";
SmtScope smts(this);
d_pfManager->translateDifficultyMap(dmap, *d_asserts);
}
-void SmtEngine::push()
+void SolverEngine::push()
{
SmtScope smts(this);
finishInit();
d_state->userPush();
}
-void SmtEngine::pop()
+void SolverEngine::pop()
{
SmtScope smts(this);
finishInit();
// clear the learned literals from the preprocessor
d_pp->clearLearnedLiterals();
- Trace("userpushpop") << "SmtEngine: popped to level "
+ Trace("userpushpop") << "SolverEngine: popped to level "
<< getUserContext()->getLevel() << endl;
// should we reset d_status here?
// SMT-LIBv2 spec seems to imply no, but it would make sense to..
}
-void SmtEngine::resetAssertions()
+void SolverEngine::resetAssertions()
{
SmtScope smts(this);
d_smtSolver->resetAssertions();
}
-void SmtEngine::interrupt()
+void SolverEngine::interrupt()
{
if (!d_state->isFullyInited())
{
d_smtSolver->interrupt();
}
-void SmtEngine::setResourceLimit(uint64_t units, bool cumulative)
+void SolverEngine::setResourceLimit(uint64_t units, bool cumulative)
{
if (cumulative)
{
d_env->d_options.base.perCallResourceLimit = units;
}
}
-void SmtEngine::setTimeLimit(uint64_t millis)
+void SolverEngine::setTimeLimit(uint64_t millis)
{
d_env->d_options.base.perCallMillisecondLimit = millis;
}
-unsigned long SmtEngine::getResourceUsage() const
+unsigned long SolverEngine::getResourceUsage() const
{
return getResourceManager()->getResourceUsage();
}
-unsigned long SmtEngine::getTimeUsage() const
+unsigned long SolverEngine::getTimeUsage() const
{
return getResourceManager()->getTimeUsage();
}
-unsigned long SmtEngine::getResourceRemaining() const
+unsigned long SolverEngine::getResourceRemaining() const
{
return getResourceManager()->getResourceRemaining();
}
-NodeManager* SmtEngine::getNodeManager() const
+NodeManager* SolverEngine::getNodeManager() const
{
return d_env->getNodeManager();
}
-void SmtEngine::printStatisticsSafe(int fd) const
+void SolverEngine::printStatisticsSafe(int fd) const
{
d_env->getStatisticsRegistry().printSafe(fd);
}
-void SmtEngine::printStatisticsDiff() const
+void SolverEngine::printStatisticsDiff() const
{
d_env->getStatisticsRegistry().printDiff(*d_env->getOptions().base.err);
d_env->getStatisticsRegistry().storeSnapshot();
}
-void SmtEngine::setOption(const std::string& key, const std::string& value)
+void SolverEngine::setOption(const std::string& key, const std::string& value)
{
Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
options::set(getOptions(), key, optionarg);
}
-void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
+void SolverEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
-bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
+bool SolverEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
-std::string SmtEngine::getOption(const std::string& key) const
+std::string SolverEngine::getOption(const std::string& key) const
{
NodeManager* nm = d_env->getNodeManager();
return options::get(getOptions(), key);
}
-Options& SmtEngine::getOptions() { return d_env->d_options; }
+Options& SolverEngine::getOptions() { return d_env->d_options; }
-const Options& SmtEngine::getOptions() const { return d_env->getOptions(); }
+const Options& SolverEngine::getOptions() const { return d_env->getOptions(); }
-ResourceManager* SmtEngine::getResourceManager() const
+ResourceManager* SolverEngine::getResourceManager() const
{
return d_env->getResourceManager();
}
-DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); }
+DumpManager* SolverEngine::getDumpManager() { return d_env->getDumpManager(); }
-const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); }
+const Printer& SolverEngine::getPrinter() const { return d_env->getPrinter(); }
-OutputManager& SmtEngine::getOutputManager() { return d_outMgr; }
+OutputManager& SolverEngine::getOutputManager() { return d_outMgr; }
-theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); }
+theory::Rewriter* SolverEngine::getRewriter() { return d_env->getRewriter(); }
} // namespace cvc5
* directory for licensing information.
* ****************************************************************************
*
- * SmtEngine: the main public entry point of libcvc5.
+ * SolverEngine: the main public entry point of libcvc5.
*/
#include "cvc5_public.h"
-#ifndef CVC5__SMT_ENGINE_H
-#define CVC5__SMT_ENGINE_H
+#ifndef CVC5__SOLVER_ENGINE_H
+#define CVC5__SOLVER_ENGINE_H
#include <map>
#include <memory>
/* -------------------------------------------------------------------------- */
-class CVC5_EXPORT SmtEngine
+class CVC5_EXPORT SolverEngine
{
friend class ::cvc5::api::Solver;
friend class ::cvc5::smt::SmtEngineState;
/* ....................................................................... */
/**
- * Construct an SmtEngine with the given expression manager.
+ * Construct an SolverEngine with the given expression manager.
* If provided, optr is a pointer to a set of options that should initialize
* the values of the options object owned by this class.
*/
- SmtEngine(NodeManager* nm, const Options* optr = nullptr);
+ SolverEngine(NodeManager* nm, const Options* optr = nullptr);
/** Destruct the SMT engine. */
- ~SmtEngine();
+ ~SolverEngine();
//--------------------------------------------- concerning the state
/**
- * This is the main initialization procedure of the SmtEngine.
+ * This is the main initialization procedure of the SolverEngine.
*
* Should be called whenever the final options and logic for the problem are
* set (at least, those options that are not permitted to change after
* options being set.
*
* This post-construction initialization is automatically triggered by the
- * use of the SmtEngine; e.g. when the first formula is asserted, a call
+ * use of the SolverEngine; e.g. when the first formula is asserted, a call
* to simplify() is issued, a scope is pushed, etc.
*/
void finishInit();
/**
- * Return true if this SmtEngine is fully initialized (post-construction)
+ * Return true if this SolverEngine is fully initialized (post-construction)
* by the above call.
*/
bool isFullyInited() const;
/** Set is internal subsolver.
*
- * This function is called on SmtEngine objects that are created internally.
- * It is used to mark that this SmtEngine should not perform preprocessing
- * passes that rephrase the input, such as --sygus-rr-synth-input or
+ * This function is called on SolverEngine objects that are created
+ * internally. It is used to mark that this SolverEngine should not
+ * perform preprocessing passes that rephrase the input, such as
+ * --sygus-rr-synth-input or
* --sygus-abduct.
*/
void setIsInternalSubsolver();
/**
* Get the assigned value of an expr (only if immediately preceded by a SAT
- * or NOT_ENTAILED query). Only permitted if the SmtEngine is set to operate
- * interactively and produce-models is on.
+ * or NOT_ENTAILED query). Only permitted if the SolverEngine is set to
+ * operate interactively and produce-models is on.
*
* @throw ModalException, TypeCheckingException, LogicException,
* UnsafeInterruptException
* elimination is LRA and LIA.
*
* This function returns a formula ret such that, given
- * the current set of formulas A asserted to this SmtEngine :
+ * the current set of formulas A asserted to this SolverEngine :
*
* If doFull = true, then
* - ( A ^ q ) and ( A ^ ret ) are equivalent
/**
* Get the current set of assertions. Only permitted if the
- * SmtEngine is set to operate interactively.
+ * SolverEngine is set to operate interactively.
*/
std::vector<Node> getAssertions();
/**
* Interrupt a running query. This can be called from another thread
- * or from a signal handler. Throws a ModalException if the SmtEngine
+ * or from a signal handler. Throws a ModalException if the SolverEngine
* isn't currently in a query.
*
* @throw ModalException
void interrupt();
/**
- * Set a resource limit for SmtEngine operations. This is like a time
+ * Set a resource limit for SolverEngine operations. This is like a time
* limit, but it's deterministic so that reproducible results can be
* obtained. Currently, it's based on the number of conflicts.
* However, please note that the definition may change between different
* cumulative==true replaces any cumulative resource limit currently
* in effect; a call with cumulative==false replaces any per-call
* resource limit currently in effect. Time limits can be set in
- * addition to resource limits; the SmtEngine obeys both. That means
- * that up to four independent limits can control the SmtEngine
+ * addition to resource limits; the SolverEngine obeys both. That means
+ * that up to four independent limits can control the SolverEngine
* at the same time.
*
- * When an SmtEngine is first created, it has no time or resource
+ * When an SolverEngine is first created, it has no time or resource
* limits.
*
- * Currently, these limits only cause the SmtEngine to stop what its
+ * Currently, these limits only cause the SolverEngine to stop what its
* doing when the limit expires (or very shortly thereafter); no
* heuristics are altered by the limits or the threat of them expiring.
* We reserve the right to change this in the future.
*
* @param units the resource limit, or 0 for no limit
* @param cumulative whether this resource limit is to be a cumulative
- * resource limit for all remaining calls into the SmtEngine (true), or
+ * resource limit for all remaining calls into the SolverEngine (true), or
* whether it's a per-call resource limit (false); the default is false
*/
void setResourceLimit(uint64_t units, bool cumulative = false);
/**
- * Set a per-call time limit for SmtEngine operations.
+ * Set a per-call time limit for SolverEngine operations.
*
* A per-call time limit can be set at the same time and replaces
* any per-call time limit currently in effect.
* Resource limits (either per-call or cumulative) can be set in
- * addition to a time limit; the SmtEngine obeys all three of them.
+ * addition to a time limit; the SolverEngine obeys all three of them.
*
* Note that the per-call timer only ticks away when one of the
- * SmtEngine's workhorse functions (things like assertFormula(),
+ * SolverEngine's workhorse functions (things like assertFormula(),
* checkEntailed(), checkSat(), and simplify()) are running.
* Between calls, the timer is still.
*
- * When an SmtEngine is first created, it has no time or resource
+ * When an SolverEngine is first created, it has no time or resource
* limits.
*
- * Currently, these limits only cause the SmtEngine to stop what its
+ * Currently, these limits only cause the SolverEngine to stop what its
* doing when the limit expires (or very shortly thereafter); no
* heuristics are altered by the limits or the threat of them expiring.
* We reserve the right to change this in the future.
void setTimeLimit(uint64_t millis);
/**
- * Get the current resource usage count for this SmtEngine. This
+ * Get the current resource usage count for this SolverEngine. This
* function can be used to ascertain reasonable values to pass as
* resource limits to setResourceLimit().
*/
unsigned long getResourceUsage() const;
- /** Get the current millisecond count for this SmtEngine. */
+ /** Get the current millisecond count for this SolverEngine. */
unsigned long getTimeUsage() const;
/**
- * Get the remaining resources that can be consumed by this SmtEngine
+ * Get the remaining resources that can be consumed by this SolverEngine
* according to the currently-set cumulative resource limit. If there
* is not a cumulative resource limit set, this function throws a
* ModalException.
/**
* Print statistics from the statistics registry in the env object owned by
- * this SmtEngine. Safe to use in a signal handler.
+ * this SolverEngine. Safe to use in a signal handler.
*/
void printStatisticsSafe(int fd) const;
/**
* Print the changes to the statistics from the statistics registry in the
- * env object owned by this SmtEngine since this method was called the last
+ * env object owned by this SolverEngine since this method was called the last
* time. Internally prints the diff and then stores a snapshot for the next
* call.
*/
Options& getOptions();
const Options& getOptions() const;
- /** Get a pointer to the UserContext owned by this SmtEngine. */
+ /** Get a pointer to the UserContext owned by this SolverEngine. */
context::UserContext* getUserContext();
- /** Get a pointer to the Context owned by this SmtEngine. */
+ /** Get a pointer to the Context owned by this SolverEngine. */
context::Context* getContext();
- /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
+ /** Get a pointer to the TheoryEngine owned by this SolverEngine. */
TheoryEngine* getTheoryEngine();
- /** Get a pointer to the PropEngine owned by this SmtEngine. */
+ /** Get a pointer to the PropEngine owned by this SolverEngine. */
prop::PropEngine* getPropEngine();
/** Get the resource manager of this SMT engine */
/** Get the output manager for this SMT engine */
OutputManager& getOutputManager();
- /** Get a pointer to the Rewriter owned by this SmtEngine. */
+ /** Get a pointer to the Rewriter owned by this SolverEngine. */
theory::Rewriter* getRewriter();
/**
* Get expanded assertions.
/* ....................................................................... */
// disallow copy/assignment
- SmtEngine(const SmtEngine&) = delete;
- SmtEngine& operator=(const SmtEngine&) = delete;
+ SolverEngine(const SolverEngine&) = delete;
+ SolverEngine& operator=(const SolverEngine&) = delete;
- /** Set solver instance that owns this SmtEngine. */
+ /** Set solver instance that owns this SolverEngine. */
void setSolver(api::Solver* solver) { d_solver = solver; }
- /** Get a pointer to the (new) PfManager owned by this SmtEngine. */
+ /** Get a pointer to the (new) PfManager owned by this SolverEngine. */
smt::PfManager* getPfManager() { return d_pfManager.get(); };
- /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
+ /** Get a pointer to the StatisticsRegistry owned by this SolverEngine. */
StatisticsRegistry& getStatisticsRegistry();
/**
std::vector<Node> getAssertionsInternal();
/* Members -------------------------------------------------------------- */
- /** Solver instance that owns this SmtEngine instance. */
+ /** Solver instance that owns this SolverEngine instance. */
api::Solver* d_solver = nullptr;
/**
*/
std::unique_ptr<Env> d_env;
/**
- * The state of this SmtEngine, which is responsible for maintaining which
+ * The state of this SolverEngine, which is responsible for maintaining which
* SMT mode we are in, the contexts, the last result, etc.
*/
std::unique_ptr<smt::SmtEngineState> d_state;
*/
std::unique_ptr<smt::Preprocessor> d_pp;
/**
- * The global scope object. Upon creation of this SmtEngine, it becomes the
- * SmtEngine in scope. It says the SmtEngine in scope until it is destructed,
- * or another SmtEngine is created.
+ * The global scope object. Upon creation of this SolverEngine, it becomes the
+ * SolverEngine in scope. It says the SolverEngine in scope until it is
+ * destructed, or another SolverEngine is created.
*/
std::unique_ptr<smt::SmtScope> d_scope;
-}; /* class SmtEngine */
+}; /* class SolverEngine */
/* -------------------------------------------------------------------------- */
for (Node conj : conjs)
{
// Start new SMT engine to check solutions
- std::unique_ptr<SmtEngine> solChecker;
+ std::unique_ptr<SolverEngine> solChecker;
initializeSubsolver(solChecker, d_env);
solChecker->getOptions().smt.checkSynthSol = false;
solChecker->getOptions().quantifiers.sygusRecFun = false;
* directory for licensing information.
* ****************************************************************************
*
- * Implementation of the unsat core manager of SmtEngine.
+ * Implementation of the unsat core manager of SolverEngine.
*/
#include "unsat_core_manager.h"
* directory for licensing information.
* ****************************************************************************
*
- * The unsat core manager of SmtEngine.
+ * The unsat core manager of SolverEngine.
*/
#include "cvc5_private.h"
class Assertions;
/**
- * This class is responsible for managing the proof output of SmtEngine, as
+ * This class is responsible for managing the proof output of SolverEngine, as
* well as setting up the global proof checker and proof node manager.
*/
class UnsatCoreManager
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
// An UnknownTypeException means that this node has no type. For now,
// only abstract values are like this---and then, only if they are created
- // by the user and don't actually correspond to one that the SmtEngine gave
- // them previously.
+ // by the user and don't actually correspond to one that the SolverEngine
+ // gave them previously.
throw UnknownTypeException(n);
}
};/* class AbstractValueTypeRule */
/** the granularity to use in the translation */
uint64_t d_granularity;
- /** an SmtEngine for context */
+ /** an SolverEngine for context */
context::Context* d_context;
/** true iff the translator should introduce
// // NOTE: Cannot have static fields like this, or else you can't have
// // two SmtEngines in the process (the second-to-be-destroyed will
// // have a dangling pointer and segfault). If this statistic is needed,
- // // fix the rewriter by making it an instance per-SmtEngine (instead of
+ // // fix the rewriter by making it an instance per-SolverEngine (instead of
// // static).
// static RuleStatistics* s_statistics;
* the conversion from external to internal selectors is done in
* expandDefinition. This invariant ensures that the rewritten form of a node
* does not mix multiple option settings, which would lead to e.g. shared
- * selectors being used in an SmtEngine instance where they are disabled.
+ * selectors being used in an SolverEngine instance where they are disabled.
*/
class DatatypesRewriter : public TheoryRewriter
{
/**
* A LogicInfo instance describes a collection of theory modules and some
* basic configuration about them. Conceptually, it provides a background
- * context for all operations in cvc5. Typically, when cvc5's SmtEngine
+ * context for all operations in cvc5. Typically, when cvc5's SolverEngine
* is created, it is issued a setLogic() command indicating features of the
* assertions and queries to follow---for example, whether quantifiers are
* used, whether integers or reals (or both) will be used, etc.
*
* Most places in cvc5 will only ever need to access a const reference to an
- * instance of this class. Such an instance is generally set by the SmtEngine
- * when setLogic() is called. However, mutating member functions are also
- * provided by this class so that it can be used as a more general mechanism
- * (e.g., for communicating to the SmtEngine which theories should be used,
- * rather than having to provide an SMT-LIB string).
+ * instance of this class. Such an instance is generally set by the
+ * SolverEngine when setLogic() is called. However, mutating member functions
+ * are also provided by this class so that it can be used as a more general
+ * mechanism (e.g., for communicating to the SolverEngine which theories should
+ * be used, rather than having to provide an SMT-LIB string).
*/
class CVC5_EXPORT LogicInfo
{
Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
// Notice we don't set produce-models. rrChecker takes the same
- // options as the SmtEngine we belong to, where we ensure that
+ // options as the SolverEngine we belong to, where we ensure that
// produce-models is set.
- std::unique_ptr<SmtEngine> rrChecker;
+ std::unique_ptr<SolverEngine> rrChecker;
initializeChecker(rrChecker, crr);
Result r = rrChecker->checkSat();
Trace("rr-check") << "...result : " << r << std::endl;
* of this class are to perform the "equivalence checking" and "congruence
* and matching filtering" in Figure 1. The equivalence checking is done
* through a combination of the sygus sampler object owned by this class
- * and the calls made to copies of the SmtEngine in ::addTerm. The rewrite
+ * and the calls made to copies of the SolverEngine in ::addTerm. The rewrite
* rule filtering (based on congruence, matching, variable ordering) is also
* managed by the sygus sampler object.
*/
Trace("cegqi-nested-qe") << " Apply qe to " << q << std::endl;
NodeManager* nm = NodeManager::currentNM();
q = nm->mkNode(kind::EXISTS, q[0], q[1].negate());
- std::unique_ptr<SmtEngine> smt_qe;
+ std::unique_ptr<SolverEngine> smt_qe;
initializeSubsolver(smt_qe, env);
Node qqe = smt_qe->getQuantifierElimination(q, true, false);
if (expr::hasBoundVar(qqe))
d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end());
}
-void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
+void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
Node query)
{
Assert (!query.isNull());
return Result(Result::SAT);
}
}
- std::unique_ptr<SmtEngine> smte;
+ std::unique_ptr<SolverEngine> smte;
initializeChecker(smte, query);
return smte->checkSat();
}
namespace cvc5 {
class Env;
-class SmtEngine;
+class SolverEngine;
namespace theory {
namespace quantifiers {
* of the argument "query", which is a formula whose free variables (of
* kind BOUND_VARIABLE) are a subset of d_vars.
*/
- void initializeChecker(std::unique_ptr<SmtEngine>& smte, Node query);
+ void initializeChecker(std::unique_ptr<SolverEngine>& smte, Node query);
/**
* Run the satisfiability check on query and return the result
* (sat/unsat/unknown).
{
Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl;
// make the satisfiability query
- std::unique_ptr<SmtEngine> queryChecker;
+ std::unique_ptr<SolverEngine> queryChecker;
initializeChecker(queryChecker, qy);
Result r = queryChecker->checkSat();
Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl;
siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr);
}
// solve the single invocation conjecture using a fresh copy of SMT engine
- std::unique_ptr<SmtEngine> siSmt;
+ std::unique_ptr<SolverEngine> siSmt;
initializeSubsolver(siSmt, d_env);
// do not use shared selectors in subsolver, since this leads to solutions
// with non-user symbols
return true;
}
-void CegisCoreConnective::getModel(SmtEngine& smt,
+void CegisCoreConnective::getModel(SolverEngine& smt,
std::vector<Node>& vals) const
{
for (const Node& v : d_vars)
}
bool CegisCoreConnective::getUnsatCore(
- SmtEngine& smt,
+ SolverEngine& smt,
const std::unordered_set<Node>& queryAsserts,
std::vector<Node>& uasserts) const
{
{
addSuccess = false;
// try a new core
- std::unique_ptr<SmtEngine> checkSol;
+ std::unique_ptr<SolverEngine> checkSol;
initializeSubsolver(checkSol, d_env);
Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
std::vector<Node> rasserts = asserts;
{
// In terms of Variant #2, this is the check "if S ^ U is unsat"
Trace("sygus-ccore") << "----- Check side condition" << std::endl;
- std::unique_ptr<SmtEngine> checkSc;
+ std::unique_ptr<SolverEngine> checkSc;
initializeSubsolver(checkSc, d_env);
std::vector<Node> scasserts;
scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
namespace cvc5 {
-class SmtEngine;
+class SolverEngine;
namespace theory {
namespace quantifiers {
* Assuming smt has just been called to check-sat and returned "SAT", this
* method adds the model for d_vars to mvs.
*/
- void getModel(SmtEngine& smt, std::vector<Node>& mvs) const;
+ void getModel(SolverEngine& smt, std::vector<Node>& mvs) const;
/**
* Assuming smt has just been called to check-sat and returned "UNSAT", this
* method get the unsat core and adds it to uasserts.
* If one of the formulas in queryAsserts was in the unsat core, then this
* method returns true. Otherwise, this method returns false.
*/
- bool getUnsatCore(SmtEngine& smt,
+ bool getUnsatCore(SolverEngine& smt,
const std::unordered_set<Node>& queryAsserts,
std::vector<Node>& uasserts) const;
/**
Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
}
-bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp)
+bool SygusInterpol::findInterpol(SolverEngine* subSolver,
+ Node& interpol,
+ Node itp)
{
// get the synthesis solution
std::map<Node, Node> sols;
if (its == sols.end())
{
Trace("sygus-interpol")
- << "SmtEngine::getInterpol: could not find solution!" << std::endl;
+ << "SolverEngine::getInterpol: could not find solution!" << std::endl;
throw RecoverableModalException(
"Could not find solution for get-interpol.");
return false;
}
- Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is "
+ Trace("sygus-interpol") << "SolverEngine::getInterpol: solution is "
<< its->second << std::endl;
interpol = its->second;
// replace back the created variables to original symbols.
Node itp = mkPredicate(name);
mkSygusConjecture(itp, axioms, conj);
- std::unique_ptr<SmtEngine> subSolver;
+ std::unique_ptr<SolverEngine> subSolver;
initializeSubsolver(subSolver, d_env);
// get the logic
LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy();
}
std::vector<Node> vars_empty;
subSolver->declareSynthFun(itp, grammarType, false, vars_empty);
- Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : "
+ Trace("sygus-interpol") << "SolverEngine::getInterpol: made conjecture : "
<< d_sygusConj << ", solving for "
<< d_sygusConj[0][0] << std::endl;
subSolver->assertSygusConstraint(d_sygusConj);
- Trace("sygus-interpol") << " SmtEngine::getInterpol check sat..."
+ Trace("sygus-interpol") << " SolverEngine::getInterpol check sat..."
<< std::endl;
Result r = subSolver->checkSynth();
- Trace("sygus-interpol") << " SmtEngine::getInterpol result: " << r
+ Trace("sygus-interpol") << " SolverEngine::getInterpol result: " << r
<< std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
namespace cvc5 {
class Env;
-class SmtEngine;
+class SolverEngine;
namespace theory {
namespace quantifiers {
* @param interpol the solution to the sygus conjecture.
* @param itp the interpolation predicate.
*/
- bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);
+ bool findInterpol(SolverEngine* subsolver, Node& interpol, Node itp);
/**
* symbols from axioms and conjecture.
*/
return Node::null();
}
// create new smt engine to do quantifier elimination
- std::unique_ptr<SmtEngine> smt_qe;
+ std::unique_ptr<SolverEngine> smt_qe;
initializeSubsolver(smt_qe, d_env);
Trace("cegqi-qep") << "Property is non-ground single invocation, run "
"QE to obtain single invocation."
Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
// make the satisfiability query
- std::unique_ptr<SmtEngine> repcChecker;
+ std::unique_ptr<SolverEngine> repcChecker;
// initialize the subsolver using the standard method
initializeSubsolver(
repcChecker,
* forall x. P( (\x. t[x,c']), x ) [***]
* is satisfiable, where notice that the above formula after beta-reduction may
* be one in pure first-order logic in a decidable theory (say linear
- * arithmetic). To check this, we invoke a separate instance of the SmtEngine
+ * arithmetic). To check this, we invoke a separate instance of the SolverEngine
* within repairSolution(...) below, which if satisfiable gives us the
* valuation for c'.
*/
Rewriter* Rewriter::getInstance()
{
- return smt::currentSmtEngine()->getRewriter();
+ return smt::currentSolverEngine()->getRewriter();
}
Node Rewriter::rewriteTo(theory::TheoryId theoryId,
private:
/**
- * Get the rewriter associated with the SmtEngine in scope.
+ * Get the rewriter associated with the SolverEngine in scope.
*
* TODO(#3468): Get rid of this function (it relies on there being an
- * singleton with the current SmtEngine in scope)
+ * singleton with the current SolverEngine in scope)
*/
static Rewriter* getInstance();
* ****************************************************************************
*
* Implementation of utilities for initializing subsolvers (copies of
- * SmtEngine) during solving.
+ * SolverEngine) during solving.
*/
#include "theory/smt_engine_subsolver.h"
return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
}
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
const Options& opts,
const LogicInfo& logicInfo,
bool needsTimeout,
unsigned long timeout)
{
NodeManager* nm = NodeManager::currentNM();
- smte.reset(new SmtEngine(nm, &opts));
+ smte.reset(new SolverEngine(nm, &opts));
smte->setIsInternalSubsolver();
smte->setLogic(logicInfo);
// set the options
smte->setTimeLimit(timeout);
}
}
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
const Env& env,
bool needsTimeout,
unsigned long timeout)
smte, env.getOptions(), env.getLogicInfo(), needsTimeout, timeout);
}
-Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
+Result checkWithSubsolver(std::unique_ptr<SolverEngine>& smte,
Node query,
const Options& opts,
const LogicInfo& logicInfo,
}
return r;
}
- std::unique_ptr<SmtEngine> smte;
+ std::unique_ptr<SolverEngine> smte;
initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout);
smte->assertFormula(query);
r = smte->checkSat();
* directory for licensing information.
* ****************************************************************************
*
- * Utilities for initializing subsolvers (copies of SmtEngine) during solving.
+ * Utilities for initializing subsolvers (copies of SolverEngine) during
+ * solving.
*/
#include "cvc5_private.h"
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
const Options& opts,
const LogicInfo& logicInfo,
bool needsTimeout = false,
/**
* Version that uses the options and logicInfo in an environment.
*/
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
const Env& env,
bool needsTimeout = false,
unsigned long timeout = 0);
* If necessary, smte is initialized to the SMT engine that checked its
* satisfiability.
*/
-Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
+Result checkWithSubsolver(std::unique_ptr<SolverEngine>& smte,
Node query,
const Options& opts,
const LogicInfo& logicInfo,
* Construct a Theory.
*
* The pair <id, instance> is assumed to uniquely identify this Theory
- * w.r.t. the SmtEngine.
+ * w.r.t. the SolverEngine.
*/
Theory(TheoryId id,
Env& env,
*/
bool isRelevant(Node lit) const;
/**
- * This is called at shutdown time by the SmtEngine, just before
+ * This is called at shutdown time by the SolverEngine, just before
* destruction. It is important because there are destruction
* ordering issues between PropEngine and Theory.
*/
void beginCall();
/**
- * Marks the end of a SmtEngine check call, stops the per
+ * Marks the end of a SolverEngine check call, stops the per
* call timer.
*/
void endCall();
* directory for licensing information.
* ****************************************************************************
*
- * A simple test for SmtEngine::resetAssertions()
+ * A simple test for SolverEngine::resetAssertions()
*
* This program indirectly also tests some corner cases w.r.t.
* context-dependent datastructures: resetAssertions() pops the contexts to
Options opts;
opts.base.outputLanguage = Language::LANG_AST;
opts.base.outputLanguageWasSetByUser = true;
- d_smt.reset(new SmtEngine(d_nodeManager, &opts));
+ d_slvEngine.reset(new SolverEngine(d_nodeManager, &opts));
}
- std::unique_ptr<SmtEngine> d_smt;
+ std::unique_ptr<SolverEngine> d_slvEngine;
bool imp(bool a, bool b) const { return (!a) || (b); }
bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); }
void SetUp() override
{
TestNode::SetUp();
- d_smt.reset(new SmtEngine(d_nodeManager));
+ d_slvEngine.reset(new SolverEngine(d_nodeManager));
}
- std::unique_ptr<SmtEngine> d_smt;
+ std::unique_ptr<SolverEngine> d_slvEngine;
};
TEST_F(TestNodeWhiteTypeNode, sub_types)
Node lambda = d_nodeManager->mkVar("lambda", funtype);
std::vector<Node> formals;
formals.push_back(x);
- d_smt->defineFunction(lambda, formals, xPos);
+ d_slvEngine->defineFunction(lambda, formals, xPos);
ASSERT_FALSE(realType.isComparableTo(booleanType));
ASSERT_TRUE(realType.isComparableTo(integerType));
TestSmt::SetUp();
d_preprocContext.reset(new preprocessing::PreprocessingPassContext(
- d_smtEngine.get(), d_smtEngine->getEnv(), nullptr));
+ d_slvEngine.get(), d_slvEngine->getEnv(), nullptr));
d_bv_gauss.reset(new BVGauss(d_preprocContext.get()));
TEST_F(TestPPWhiteForeignTheoryRewrite, simplify)
{
- ForeignTheoryRewriter ftr(d_smtEngine->getEnv());
+ ForeignTheoryRewriter ftr(d_slvEngine->getEnv());
std::cout << "len(x) >= 0 is simplified to true" << std::endl;
Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType());
Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x);
void SetUp() override
{
TestSmt::SetUp();
- d_theoryEngine = d_smtEngine->getTheoryEngine();
+ d_theoryEngine = d_slvEngine->getTheoryEngine();
d_satSolver.reset(new FakeSatSolver());
d_cnfContext.reset(new context::Context());
d_cnfRegistrar.reset(new prop::NullRegistrar);
new cvc5::prop::CnfStream(d_satSolver.get(),
d_cnfRegistrar.get(),
d_cnfContext.get(),
- &d_smtEngine->getEnv(),
- d_smtEngine->getResourceManager()));
+ &d_slvEngine->getEnv(),
+ d_slvEngine->getResourceManager()));
}
void TearDown() override
* directory for licensing information.
* ****************************************************************************
*
- * Common header for unit tests that need an SmtEngine.
+ * Common header for unit tests that need an SolverEngine.
*/
#ifndef CVC5__TEST__UNIT__TEST_SMT_H
d_nodeManager = NodeManager::currentNM();
d_nodeManager->init();
d_skolemManager = d_nodeManager->getSkolemManager();
- d_smtEngine.reset(new SmtEngine(d_nodeManager));
- d_smtEngine->finishInit();
+ d_slvEngine.reset(new SolverEngine(d_nodeManager));
+ d_slvEngine->finishInit();
}
NodeManager* d_nodeManager;
SkolemManager* d_skolemManager;
- std::unique_ptr<SmtEngine> d_smtEngine;
+ std::unique_ptr<SolverEngine> d_slvEngine;
};
class TestSmtNoFinishInit : public TestInternal
d_nodeManager = NodeManager::currentNM();
d_nodeManager->init();
d_skolemManager = d_nodeManager->getSkolemManager();
- d_smtEngine.reset(new SmtEngine(d_nodeManager));
+ d_slvEngine.reset(new SolverEngine(d_nodeManager));
}
NodeManager* d_nodeManager;
SkolemManager* d_skolemManager;
- std::unique_ptr<SmtEngine> d_smtEngine;
+ std::unique_ptr<SolverEngine> d_slvEngine;
};
/* -------------------------------------------------------------------------- */
std::vector<Node> args = {w, x, y, z};
std::vector<Node> vals = {c1, zero, one, c1};
- Rewriter* rr = d_smtEngine->getRewriter();
+ Rewriter* rr = d_slvEngine->getRewriter();
Evaluator eval(rr);
Node r = eval.eval(t, args, vals);
ASSERT_EQ(r,
std::vector<Node> args = {x};
std::vector<Node> vals = {c};
- Rewriter* rr = d_smtEngine->getRewriter();
+ Rewriter* rr = d_slvEngine->getRewriter();
Evaluator eval(rr);
Node r = eval.eval(t, args, vals);
ASSERT_EQ(r,
std::vector<Node> args;
std::vector<Node> vals;
- Rewriter* rr = d_smtEngine->getRewriter();
+ Rewriter* rr = d_slvEngine->getRewriter();
Evaluator eval(rr);
{
std::vector<Node> args;
std::vector<Node> vals;
- Rewriter* rr = d_smtEngine->getRewriter();
+ Rewriter* rr = d_slvEngine->getRewriter();
Evaluator eval(rr);
// (str.code "A") ---> 65
{
TestSmt::SetUp();
Options opts;
- d_rewriter = d_smtEngine->getRewriter();
+ d_rewriter = d_slvEngine->getRewriter();
d_seqRewriter.reset(new SequencesRewriter(d_rewriter, nullptr));
}
void SetUp() override
{
TestSmtNoFinishInit::SetUp();
- d_smtEngine->setOption("produce-models", "true");
- d_smtEngine->finishInit();
+ d_slvEngine->setOption("produce-models", "true");
+ d_slvEngine->finishInit();
d_true = d_nodeManager->mkConst<bool>(true);
d_one = d_nodeManager->mkConst<Rational>(Rational(1));
}
void SetUp() override
{
TestSmtNoFinishInit::SetUp();
- d_smtEngine->setOption("incremental", "false");
- d_smtEngine->finishInit();
+ d_slvEngine->setOption("incremental", "false");
+ d_slvEngine->finishInit();
d_arith = static_cast<TheoryArith*>(
- d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
+ d_slvEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
d_realType.reset(new TypeNode(d_nodeManager->realType()));
d_intType.reset(new TypeNode(d_nodeManager->integerType()));
void fakeTheoryEnginePreprocess(TNode input)
{
Assert(input == Rewriter::rewrite(input));
- d_smtEngine->getTheoryEngine()->preRegister(input);
+ d_slvEngine->getTheoryEngine()->preRegister(input);
}
Theory::Effort d_level = Theory::EFFORT_FULL;
void SetUp() override
{
TestSmtNoFinishInit::SetUp();
- d_smtEngine->setOption("produce-models", "true");
- d_smtEngine->finishInit();
+ d_slvEngine->setOption("produce-models", "true");
+ d_slvEngine->finishInit();
d_true = d_nodeManager->mkConst<bool>(true);
d_one = d_nodeManager->mkConst<Rational>(Rational(1));
}
// translating it to integers should yield 7.
IntBlaster intBlaster(
- d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, false);
+ d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, false);
Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems);
Node seven = d_nodeManager->mkConst(Rational(7));
ASSERT_EQ(seven, result);
// translating it to integers should yield an integer variable.
IntBlaster intBlaster(
- d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
+ d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
Node result = intBlaster.translateNoChildren(bv, lemmas, skolems);
ASSERT_TRUE(result.isVar() && result.getType().isInteger());
// translating it to integers should yield an Int x Int -> Bool function
IntBlaster intBlaster(
- d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
+ d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
Node result = intBlaster.translateNoChildren(f, lemmas, skolems);
TypeNode resultType = result.getType();
std::vector<TypeNode> resultDomain = resultType.getArgTypes();
std::vector<Node> lemmas;
std::map<Node, Node> skolems;
IntBlaster intBlaster(
- d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
+ d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
// bit-vector variables
TypeNode bvType = d_nodeManager->mkBitVectorType(4);
void SetUp() override
{
TestSmtNoFinishInit::SetUp();
- d_smtEngine->setOption("produce-assertions", "true");
- d_smtEngine->finishInit();
+ d_slvEngine->setOption("produce-assertions", "true");
+ d_slvEngine->finishInit();
- d_optslv.reset(new OptimizationSolver(d_smtEngine.get()));
+ d_optslv.reset(new OptimizationSolver(d_slvEngine.get()));
d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u)));
d_BV16Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(16u)));
}
Node b = d_nodeManager->mkConst(BitVector(32u, (unsigned)0xFFFFFFF1));
// (unsigned)0x3FFFFFA1 <= x <= (unsigned)0xFFFFFFF1
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x));
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b));
d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, (uint32_t)0x3FFFFFA1));
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteBVOpt, signed_min)
Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000));
Node b = d_nodeManager->mkConst(BitVector(32u, 2147483647u));
// -2147483648 <= x <= 2147483647
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x));
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b));
d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true);
// expect the minimum x = -1
ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000));
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
// If the gap is too large, it will have a performance issue!!!
// Need binary search!
// (unsigned)1 <= x <= (unsigned)2
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x));
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b));
d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false);
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, 2u));
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteBVOpt, signed_max)
Node b = d_nodeManager->mkConst(BitVector(32u, 10u));
// -2147483648 <= x <= 10
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x));
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b));
d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true);
// expect the maxmum x =
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, 10u));
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteBVOpt, min_boundary)
Node y = d_nodeManager->mkVar(*d_BV32Type);
// x <= 18
- d_smtEngine->assertFormula(d_nodeManager->mkNode(
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(
kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
// this perturbs the solver to trigger some boundary bug
// that existed previously
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
// expect the maximum x = 18
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, 18u));
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
} // namespace test
TEST_F(TestTheoryWhiteBv, bitblaster_core)
{
- d_smtEngine->setLogic("QF_BV");
+ d_slvEngine->setLogic("QF_BV");
- d_smtEngine->setOption("bitblast", "eager");
- d_smtEngine->setOption("bv-solver", "layered");
- d_smtEngine->setOption("incremental", "false");
+ d_slvEngine->setOption("bitblast", "eager");
+ d_slvEngine->setOption("bv-solver", "layered");
+ d_slvEngine->setOption("incremental", "false");
// Notice that this unit test uses the theory engine of a created SMT
- // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized
+ // engine d_slvEngine. We must ensure that d_slvEngine is properly initialized
// via the following call, which constructs its underlying theory engine.
- d_smtEngine->finishInit();
+ d_slvEngine->finishInit();
TheoryBV* tbv = dynamic_cast<TheoryBV*>(
- d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]);
+ d_slvEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]);
BVSolverLayered* bvsl = dynamic_cast<BVSolverLayered*>(tbv->d_internal.get());
std::unique_ptr<EagerBitblaster> bb(
- new EagerBitblaster(bvsl, d_smtEngine->getContext()));
+ new EagerBitblaster(bvsl, d_slvEngine->getContext()));
Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16));
Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16));
TEST_F(TestTheoryWhiteBv, mkUmulo)
{
- d_smtEngine->setOption("incremental", "true");
+ d_slvEngine->setOption("incremental", "true");
for (uint32_t w = 1; w < 16; ++w)
{
- d_smtEngine->push();
+ d_slvEngine->push();
Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(w));
Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(w));
kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w));
Node rhs = mkUmulo(x, y);
Node eq = d_nodeManager->mkNode(kind::DISTINCT, lhs, rhs);
- d_smtEngine->assertFormula(eq);
- Result res = d_smtEngine->checkSat();
+ d_slvEngine->assertFormula(eq);
+ Result res = d_slvEngine->checkSat();
ASSERT_EQ(res.isSat(), Result::UNSAT);
- d_smtEngine->pop();
+ d_slvEngine->pop();
}
}
} // namespace test
void SetUp() override
{
TestSmt::SetUp();
- d_context = d_smtEngine->getContext();
- d_user_context = d_smtEngine->getUserContext();
+ d_context = d_slvEngine->getContext();
+ d_user_context = d_slvEngine->getUserContext();
- d_theoryEngine = d_smtEngine->getTheoryEngine();
+ d_theoryEngine = d_slvEngine->getTheoryEngine();
for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id)
{
delete d_theoryEngine->d_theoryOut[id];
void SetUp() override
{
TestSmtNoFinishInit::SetUp();
- d_smtEngine->setOption("produce-assertions", "true");
- d_smtEngine->finishInit();
+ d_slvEngine->setOption("produce-assertions", "true");
+ d_slvEngine->finishInit();
- d_optslv.reset(new OptimizationSolver(d_smtEngine.get()));
+ d_optslv.reset(new OptimizationSolver(d_slvEngine.get()));
d_intType.reset(new TypeNode(d_nodeManager->integerType()));
}
/* Result of asserts is:
0 < max_cost < 100
*/
- d_smtEngine->assertFormula(upb);
- d_smtEngine->assertFormula(lowb);
+ d_slvEngine->assertFormula(upb);
+ d_slvEngine->assertFormula(lowb);
// We activate our objective so the subsolver knows to optimize it
d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Rational("99"));
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteIntOpt, min)
/* Result of asserts is:
0 < max_cost < 100
*/
- d_smtEngine->assertFormula(upb);
- d_smtEngine->assertFormula(lowb);
+ d_slvEngine->assertFormula(upb);
+ d_slvEngine->assertFormula(lowb);
// We activate our objective so the subsolver knows to optimize it
d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE);
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Rational("1"));
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteIntOpt, result)
/* Result of asserts is:
0 > max_cost > 100
*/
- d_smtEngine->assertFormula(upb);
- d_smtEngine->assertFormula(lowb);
+ d_slvEngine->assertFormula(upb);
+ d_slvEngine->assertFormula(lowb);
// We activate our objective so the subsolver knows to optimize it
d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
// We expect our check to have returned UNSAT
ASSERT_EQ(r.isSat(), Result::UNSAT);
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteIntOpt, open_interval)
0 < cost1 < 100
110 < cost2
*/
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1));
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1));
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2));
/* Optimization objective:
cost1 + cost2
// expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Rational("112"));
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
}
} // namespace test
void SetUp() override
{
TestSmtNoFinishInit::SetUp();
- d_smtEngine->setOption("produce-assertions", "true");
- d_smtEngine->finishInit();
+ d_slvEngine->setOption("produce-assertions", "true");
+ d_slvEngine->finishInit();
d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u)));
}
TEST_F(TestTheoryWhiteOptMultigoal, box)
{
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
Node x = d_nodeManager->mkVar(*d_BV32Type);
Node y = d_nodeManager->mkVar(*d_BV32Type);
Node z = d_nodeManager->mkVar(*d_BV32Type);
// 18 <= x
- d_smtEngine->assertFormula(d_nodeManager->mkNode(
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(
kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
// y <= x
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
- OptimizationSolver optSolver(d_smtEngine.get());
+ OptimizationSolver optSolver(d_slvEngine.get());
// minimize x
optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
TEST_F(TestTheoryWhiteOptMultigoal, lex)
{
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
Node x = d_nodeManager->mkVar(*d_BV32Type);
Node y = d_nodeManager->mkVar(*d_BV32Type);
Node z = d_nodeManager->mkVar(*d_BV32Type);
// 18 <= x
- d_smtEngine->assertFormula(d_nodeManager->mkNode(
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(
kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
// y <= x
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
- OptimizationSolver optSolver(d_smtEngine.get());
+ OptimizationSolver optSolver(d_slvEngine.get());
// minimize x
optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
TEST_F(TestTheoryWhiteOptMultigoal, pareto)
{
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
TypeNode bv4ty(d_nodeManager->mkBitVectorType(4u));
Node a = d_nodeManager->mkVar(bv4ty);
Node b = d_nodeManager->mkVar(bv4ty);
(and (= a 1) (= b 3))
))
*/
- d_smtEngine->assertFormula(d_nodeManager->mkOr(stmts));
+ d_slvEngine->assertFormula(d_nodeManager->mkOr(stmts));
/*
(maximize a)
(maximize b)
*/
- OptimizationSolver optSolver(d_smtEngine.get());
+ OptimizationSolver optSolver(d_slvEngine.get());
optSolver.addObjective(a, OptimizationObjective::MAXIMIZE);
optSolver.addObjective(b, OptimizationObjective::MAXIMIZE);
TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
{
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
Node x = d_nodeManager->mkVar(*d_BV32Type);
Node y = d_nodeManager->mkVar(*d_BV32Type);
Node z = d_nodeManager->mkVar(*d_BV32Type);
// 18 <= x
- d_smtEngine->assertFormula(d_nodeManager->mkNode(
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(
kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
// y <= x
- d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+ d_slvEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
- OptimizationSolver optSolver(d_smtEngine.get());
+ OptimizationSolver optSolver(d_slvEngine.get());
// minimize x
optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
// push
- d_smtEngine->push();
+ d_slvEngine->push();
// maximize y with `signed` comparison over bit-vectors.
optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
BitVector(32u, (unsigned)0xFFFFFFFF));
// pop
- d_smtEngine->pop();
+ d_slvEngine->pop();
// now we only have one objective: (minimize x)
r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
// resetting the assertions also resets the optimization objectives
- d_smtEngine->resetAssertions();
+ d_slvEngine->resetAssertions();
r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
ASSERT_EQ(r.isSat(), Result::SAT);
results = optSolver.getValues();
void SetUp() override
{
TestSmtNoFinishInit::SetUp();
- d_smtEngine->setOption("cegqi-full", "true");
- d_smtEngine->setOption("produce-models", "true");
- d_smtEngine->finishInit();
+ d_slvEngine->setOption("cegqi-full", "true");
+ d_slvEngine->setOption("produce-models", "true");
+ d_slvEngine->finishInit();
d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4));
d_t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(4));
Node body = d_nodeManager->mkNode(k, x, d_t);
Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, body);
Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
- Result res = d_smtEngine->checkSat(a);
+ Result res = d_slvEngine->checkSat(a);
ASSERT_EQ(res.d_sat, Result::UNSAT);
}
Node scr =
d_nodeManager->mkNode(EXISTS, d_bvarlist, pol ? body : body.notNode());
Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
- Result res = d_smtEngine->checkSat(a);
+ Result res = d_slvEngine->checkSat(a);
if (res.d_sat == Result::SAT)
{
std::cout << std::endl;
- std::cout << "s " << d_smtEngine->getValue(d_s) << std::endl;
- std::cout << "t " << d_smtEngine->getValue(d_t) << std::endl;
- std::cout << "x " << d_smtEngine->getValue(d_x) << std::endl;
+ std::cout << "s " << d_slvEngine->getValue(d_s) << std::endl;
+ std::cout << "t " << d_slvEngine->getValue(d_t) << std::endl;
+ std::cout << "x " << d_slvEngine->getValue(d_x) << std::endl;
}
ASSERT_EQ(res.d_sat, Result::UNSAT);
}
Node scr =
d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
- Result res = d_smtEngine->checkSat(a);
+ Result res = d_slvEngine->checkSat(a);
if (res.d_sat == Result::SAT)
{
std::cout << std::endl;
if (!s1.isNull())
- std::cout << "s1 " << d_smtEngine->getValue(s1) << std::endl;
+ std::cout << "s1 " << d_slvEngine->getValue(s1) << std::endl;
if (!s2.isNull())
- std::cout << "s2 " << d_smtEngine->getValue(s2) << std::endl;
- std::cout << "t " << d_smtEngine->getValue(t) << std::endl;
- std::cout << "x " << d_smtEngine->getValue(x) << std::endl;
+ std::cout << "s2 " << d_slvEngine->getValue(s2) << std::endl;
+ std::cout << "t " << d_slvEngine->getValue(t) << std::endl;
+ std::cout << "x " << d_slvEngine->getValue(x) << std::endl;
}
ASSERT_TRUE(res.d_sat == Result::UNSAT);
}
Node scr =
d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
- Result res = d_smtEngine->checkSat(a);
+ Result res = d_slvEngine->checkSat(a);
if (res.d_sat == Result::SAT)
{
std::cout << std::endl;
- std::cout << "t " << d_smtEngine->getValue(t) << std::endl;
- std::cout << "x " << d_smtEngine->getValue(x) << std::endl;
+ std::cout << "t " << d_slvEngine->getValue(t) << std::endl;
+ std::cout << "x " << d_slvEngine->getValue(x) << std::endl;
}
ASSERT_TRUE(res.d_sat == Result::UNSAT);
}
void SetUp() override
{
TestSmtNoFinishInit::SetUp();
- d_smtEngine->finishInit();
- delete d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN];
- delete d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN];
- d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = nullptr;
- d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = nullptr;
+ d_slvEngine->finishInit();
+ delete d_slvEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN];
+ delete d_slvEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN];
+ d_slvEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = nullptr;
+ d_slvEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = nullptr;
d_dummy_theory.reset(new DummyTheory<THEORY_BUILTIN>(
- d_smtEngine->getEnv(), d_outputChannel, Valuation(nullptr)));
+ d_slvEngine->getEnv(), d_outputChannel, Valuation(nullptr)));
d_outputChannel.clear();
d_atom0 = d_nodeManager->mkConst(true);
d_atom1 = d_nodeManager->mkConst(false);
projects / cvc5.git / commitdiff