This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.
This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).
Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).
theory/sets/theory_sets_type_rules.h
theory/shared_terms_database.cpp
theory/shared_terms_database.h
+ theory/smt_engine_subsolver.cpp
+ theory/smt_engine_subsolver.h
theory/sort_inference.cpp
theory/sort_inference.h
theory/strings/base_solver.cpp
cardinality FUNCTION_TYPE \
"::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
"theory/builtin/theory_builtin_type_rules.h"
-well-founded FUNCTION_TYPE false
+well-founded FUNCTION_TYPE \
+ "::CVC4::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \
+ "::CVC4::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \
+ "theory/builtin/theory_builtin_type_rules.h"
enumerator FUNCTION_TYPE \
::CVC4::theory::builtin::FunctionEnumerator \
"theory/builtin/type_enumerator.h"
return valueCard ^ argsCard;
}
+ /** Function type is well-founded if its component sorts are */
+ static bool isWellFounded(TypeNode type)
+ {
+ for (TypeNode::iterator i = type.begin(), i_end = type.end(); i != i_end;
+ ++i)
+ {
+ if (!(*i).isWellFounded())
+ {
+ return false;
+ }
+ }
+ return true;
+ }
+ /**
+ * Ground term for function sorts is (lambda x. t) where x is the
+ * canonical variable list for its type and t is the canonical ground term of
+ * its range.
+ */
+ static Node mkGroundTerm(TypeNode type)
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node bvl = nm->getBoundVarListForFunctionType(type);
+ Node ret = type.getRangeType().mkGroundTerm();
+ return nm->mkNode(kind::LAMBDA, bvl, ret);
+ }
};/* class FuctionProperties */
class SExprProperties {
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/term_util.h"
+#include "theory/smt_engine_subsolver.h"
using namespace std;
using namespace CVC4::kind;
// Convert bound variables to skolems. This ensures the satisfiability
// check is ground.
Node squery = convertToSkolem(query);
- NodeManager* nm = NodeManager::currentNM();
if (options::sygusExprMinerCheckUseExport())
{
- // To support a separate timeout for the subsolver, we need to create
- // a separate ExprManager with its own options. This requires that
- // the expressions sent to the subsolver can be exported from on
- // ExprManager to another. If the export fails, we throw an
- // OptionException.
- try
- {
- checker.reset(new SmtEngine(&em));
- checker->setIsInternalSubsolver();
- checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true);
- checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
- checker->setOption("sygus-rr-synth-input", false);
- checker->setOption("input-language", "smt2");
- Expr equery = squery.toExpr().exportTo(&em, varMap);
- checker->assertFormula(equery);
- }
- catch (const CVC4::ExportUnsupportedException& e)
- {
- std::stringstream msg;
- msg << "Unable to export " << squery
- << " but exporting expressions is "
- "required for an expression "
- "miner check.";
- throw OptionException(msg.str());
- }
+ initializeSubsolverWithExport(checker,
+ em,
+ varMap,
+ squery.toExpr(),
+ true,
+ options::sygusExprMinerCheckTimeout());
+ checker->setOption("sygus-rr-synth-input", false);
+ checker->setOption("input-language", "smt2");
needExport = true;
}
else
{
+ initializeSubsolver(checker, squery.toExpr());
needExport = false;
- checker.reset(new SmtEngine(nm->toExprManager()));
- checker->assertFormula(squery.toExpr());
}
}
#include <map>
#include <memory>
#include <vector>
+#include "expr/expr.h"
#include "expr/expr_manager.h"
-#include "expr/node.h"
+#include "expr/variable_type_map.h"
#include "smt/smt_engine.h"
#include "theory/quantifiers/sygus_sampler.h"
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
#include "util/random.h"
using namespace CVC4::kind;
Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
{
- Assert(mvs.empty());
- Assert(n.getType().isBoolean());
Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
- n = Rewriter::rewrite(n);
- if (n.isConst())
- {
- if (n.getConst<bool>())
- {
- // default model
- for (const Node& v : d_vars)
- {
- mvs.push_back(v.getType().mkGroundTerm());
- }
- return Result(Result::SAT);
- }
- else
- {
- return Result(Result::UNSAT);
- }
- }
- SmtEngine smt(NodeManager::currentNM()->toExprManager());
- smt.setIsInternalSubsolver();
- smt.setLogic(smt::currentSmtEngine()->getLogicInfo());
- smt.assertFormula(n.toExpr());
- Result r = smt.checkSat();
+ Result r = checkWithSubsolver(n, d_vars, mvs);
Trace("sygus-ccore-debug") << "...got " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
- {
- getModel(smt, mvs);
- }
return r;
}
{
addSuccess = false;
// try a new core
- SmtEngine checkSol(nm->toExprManager());
- checkSol.setIsInternalSubsolver();
- checkSol.setLogic(smt::currentSmtEngine()->getLogicInfo());
+ std::unique_ptr<SmtEngine> checkSol;
+ initializeSubsolver(checkSol);
Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
std::vector<Node> rasserts = asserts;
rasserts.push_back(d_sc);
Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts);
for (const Node& a : rasserts)
{
- checkSol.assertFormula(a.toExpr());
+ checkSol->assertFormula(a.toExpr());
}
- Result r = checkSol.checkSat();
+ Result r = checkSol->checkSat();
Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl;
// In terms of Variant #2, this is the check "if (S ^ D) => B"
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
std::unordered_set<Node, NodeHashFunction> queryAsserts;
queryAsserts.insert(ccheck.getFormula());
queryAsserts.insert(d_sc);
- bool hasQuery = getUnsatCore(checkSol, queryAsserts, uasserts);
+ bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts);
// now, check the side condition
bool falseCore = false;
if (!d_sc.isNull())
{
// In terms of Variant #2, this is the check "if S ^ U is unsat"
Trace("sygus-ccore") << "----- Check side condition" << std::endl;
- SmtEngine checkSc(nm->toExprManager());
- checkSc.setIsInternalSubsolver();
- checkSc.setLogic(smt::currentSmtEngine()->getLogicInfo());
+ std::unique_ptr<SmtEngine> checkSc;
+ initializeSubsolver(checkSc);
std::vector<Node> scasserts;
scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
scasserts.push_back(d_sc);
std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom());
for (const Node& sca : scasserts)
{
- checkSc.assertFormula(sca.toExpr());
+ checkSc->assertFormula(sca.toExpr());
}
- Result rsc = checkSc.checkSat();
+ Result rsc = checkSc->checkSat();
Trace("sygus-ccore")
<< "----- check-sat returned " << rsc << std::endl;
if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT)
uasserts.clear();
std::unordered_set<Node, NodeHashFunction> queryAsserts2;
queryAsserts2.insert(d_sc);
- getUnsatCore(checkSc, queryAsserts2, uasserts);
+ getUnsatCore(*checkSc, queryAsserts2, uasserts);
falseCore = true;
}
}
// it does not entail the postcondition, add an assertion that blocks
// the current point
mvs.clear();
- getModel(checkSol, mvs);
+ getModel(*checkSol, mvs);
// should evaluate to true
Node ean = evaluate(an, Node::null(), mvs);
Assert(ean.isConst() && ean.getConst<bool>());
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
using namespace CVC4::kind;
// To support a separate timeout for the subsolver, we need to create
// a separate ExprManager with its own options. This requires that
// the expressions sent to the subsolver can be exported from on
- // ExprManager to another. If the export fails, we throw an
- // OptionException.
- try
- {
- checker.reset(new SmtEngine(&em));
- checker->setIsInternalSubsolver();
- checker->setTimeLimit(options::sygusRepairConstTimeout(), true);
- checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
- // renable options disabled by sygus
- checker->setOption("miniscope-quant", true);
- checker->setOption("miniscope-quant-fv", true);
- checker->setOption("quant-split", true);
- // export
- Expr e_query = query.toExpr().exportTo(&em, varMap);
- checker->assertFormula(e_query);
- }
- catch (const CVC4::ExportUnsupportedException& e)
- {
- std::stringstream msg;
- msg << "Unable to export " << query
- << " but exporting expressions is required for "
- "--sygus-repair-const-timeout.";
- throw OptionException(msg.str());
- }
+ // ExprManager to another.
+ initializeSubsolverWithExport(checker,
+ em,
+ varMap,
+ query.toExpr(),
+ true,
+ options::sygusRepairConstTimeout());
+ // renable options disabled by sygus
+ checker->setOption("miniscope-quant", true);
+ checker->setOption("miniscope-quant-fv", true);
+ checker->setOption("quant-split", true);
}
else
{
needExport = false;
- checker.reset(new SmtEngine(nm->toExprManager()));
- checker->assertFormula(query.toExpr());
+ initializeSubsolver(checker, query.toExpr());
}
}
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "prop/prop_engine.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
#include "theory/theory_engine.h"
using namespace CVC4::kind;
if (options::sygusVerifySubcall())
{
Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl;
- SmtEngine verifySmt(nm->toExprManager());
- verifySmt.setIsInternalSubsolver();
- verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
- verifySmt.assertFormula(query.toExpr());
- Result r = verifySmt.checkSat();
+
+ Result r =
+ checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
Trace("cegqi-engine") << " ...got " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
- Trace("cegqi-engine") << " * Verification lemma failed for:\n ";
- // do not send out
- for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
+ if (Trace.isOn("cegqi-engine"))
{
- Node v = d_ce_sk_vars[i];
- Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr()));
- Trace("cegqi-engine") << vars[i] << " -> " << mv << " ";
- d_ce_sk_var_mvs.push_back(mv);
+ Trace("cegqi-engine") << " * Verification lemma failed for:\n ";
+ for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
+ {
+ Trace("cegqi-engine")
+ << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " ";
+ }
+ Trace("cegqi-engine") << std::endl;
}
- Trace("cegqi-engine") << std::endl;
#ifdef CVC4_ASSERTIONS
// the values for the query should be a complete model
Node squery = query.substitute(d_ce_sk_vars.begin(),
{
Node sc = d_embedSideCondition.substitute(
d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end());
- sc = Rewriter::rewrite(sc);
Trace("cegqi-engine") << "Check side condition..." << std::endl;
Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
- NodeManager* nm = NodeManager::currentNM();
- SmtEngine scSmt(nm->toExprManager());
- scSmt.setIsInternalSubsolver();
- scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
- scSmt.assertFormula(sc.toExpr());
- Result r = scSmt.checkSat();
+ Result r = checkWithSubsolver(sc);
Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
if (r == Result::UNSAT)
{
#include "theory/quantifiers/sygus/synth_engine.h"
#include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
#include "theory/theory_engine.h"
using namespace CVC4::kind;
if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
{
// create new smt engine to do quantifier elimination
- SmtEngine smt_qe(nm->toExprManager());
- smt_qe.setIsInternalSubsolver();
- smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo());
+ std::unique_ptr<SmtEngine> smt_qe;
+ initializeSubsolver(smt_qe);
Trace("cegqi-qep") << "Property is non-ground single invocation, run "
"QE to obtain single invocation."
<< std::endl;
Trace("cegqi-qep") << "Run quantifier elimination on "
<< conj_se_ngsi_subs << std::endl;
- Expr qe_res = smt_qe.doQuantifierElimination(
+ Expr qe_res = smt_qe->doQuantifierElimination(
conj_se_ngsi_subs.toExpr(), true, false);
Trace("cegqi-qep") << "Result : " << qe_res << std::endl;
--- /dev/null
+/********************* */
+/*! \file smt_engine_subsolver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of utilities for initializing subsolvers (copies of
+ ** SmtEngine) during solving.
+ **/
+
+#include "theory/smt_engine_subsolver.h"
+
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+
+// optimization: try to rewrite to constant
+Result quickCheck(Node& query)
+{
+ query = theory::Rewriter::rewrite(query);
+ if (query.isConst())
+ {
+ if (!query.getConst<bool>())
+ {
+ return Result(Result::UNSAT);
+ }
+ else
+ {
+ return Result(Result::SAT);
+ }
+ }
+ return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
+}
+
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ smte.reset(new SmtEngine(nm->toExprManager()));
+ smte->setIsInternalSubsolver();
+ smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
+}
+
+void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
+ ExprManager& em,
+ ExprManagerMapCollection& varMap,
+ Node query,
+ bool needsTimeout,
+ unsigned long timeout)
+{
+ // To support a separate timeout for the subsolver, we need to use
+ // a separate ExprManager with its own options. This requires that
+ // the expressions sent to the subsolver can be exported from on
+ // ExprManager to another. If the export fails, we throw an
+ // OptionException.
+ try
+ {
+ smte.reset(new SmtEngine(&em));
+ smte->setIsInternalSubsolver();
+ if (needsTimeout)
+ {
+ smte->setTimeLimit(timeout, true);
+ }
+ smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
+ Expr equery = query.toExpr().exportTo(&em, varMap);
+ smte->assertFormula(equery);
+ }
+ catch (const CVC4::ExportUnsupportedException& e)
+ {
+ std::stringstream msg;
+ msg << "Unable to export " << query
+ << " but exporting expressions is "
+ "required for a subsolver.";
+ throw OptionException(msg.str());
+ }
+}
+
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query)
+{
+ initializeSubsolver(smte);
+ smte->assertFormula(query.toExpr());
+}
+
+Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query)
+{
+ Assert(query.getType().isBoolean());
+ Result r = quickCheck(query);
+ if (!r.isUnknown())
+ {
+ return r;
+ }
+ initializeSubsolver(smte, query);
+ return smte->checkSat();
+}
+
+Result checkWithSubsolver(Node query, bool needsTimeout, unsigned long timeout)
+{
+ std::vector<Node> vars;
+ std::vector<Node> modelVals;
+ return checkWithSubsolver(query, vars, modelVals, needsTimeout, timeout);
+}
+
+Result checkWithSubsolver(Node query,
+ const std::vector<Node>& vars,
+ std::vector<Node>& modelVals,
+ bool needsTimeout,
+ unsigned long timeout)
+{
+ Assert(query.getType().isBoolean());
+ Assert(modelVals.empty());
+ // ensure clear
+ modelVals.clear();
+ Result r = quickCheck(query);
+ if (!r.isUnknown())
+ {
+ if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ {
+ // default model
+ for (const Node& v : vars)
+ {
+ modelVals.push_back(v.getType().mkGroundTerm());
+ }
+ }
+ return r;
+ }
+ std::unique_ptr<SmtEngine> smte;
+ ExprManagerMapCollection varMap;
+ NodeManager* nm = NodeManager::currentNM();
+ ExprManager em(nm->getOptions());
+ bool needsExport = false;
+ if (needsTimeout)
+ {
+ needsExport = true;
+ initializeSubsolverWithExport(
+ smte, em, varMap, query, needsTimeout, timeout);
+ }
+ else
+ {
+ initializeSubsolver(smte, query);
+ }
+ r = smte->checkSat();
+ if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ {
+ for (const Node& v : vars)
+ {
+ Expr val;
+ if (needsExport)
+ {
+ Expr ev = v.toExpr().exportTo(&em, varMap);
+ val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap);
+ }
+ else
+ {
+ val = smte->getValue(v.toExpr());
+ }
+ modelVals.push_back(Node::fromExpr(val));
+ }
+ }
+ return r;
+}
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file smt_engine_subsolver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for initializing subsolvers (copies of SmtEngine) during
+ ** solving.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
+#define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
+
+#include <map>
+#include <memory>
+#include <vector>
+#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "expr/variable_type_map.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * This function initializes the smt engine smte as a subsolver, e.g. it
+ * creates a new SMT engine and sets the options of the current SMT engine.
+ */
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte);
+
+/**
+ * Initialize Smt subsolver with exporting
+ *
+ * This function initializes the smt engine smte to check the satisfiability
+ * of the argument "query".
+ *
+ * The arguments em and varMap are used for supporting cases where we
+ * want smte to use a different expression manager instead of the current
+ * expression manager. The motivation for this so that different options can
+ * be set for the subcall.
+ *
+ * Notice that subsequent expressions extracted from smte (for instance, model
+ * values) must be exported to the current expression
+ * manager.
+ *
+ * @param smte The smt engine pointer to initialize
+ * @param em Reference to the expression manager to use
+ * @param varMap Map used for exporting expressions
+ * @param query The query to check
+ * @param needsTimeout Whether we would like to set a timeout
+ * @param timeout The timeout (in milliseconds)
+ */
+void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
+ ExprManager& em,
+ ExprManagerMapCollection& varMap,
+ Node query,
+ bool needsTimeout = false,
+ unsigned long timeout = 0);
+
+/**
+ * This function initializes the smt engine smte to check the satisfiability
+ * of the argument "query", without exporting expressions.
+ *
+ * Notice that is not possible to set a timeout value currently without
+ * exporting since the Options and ExprManager are tied together.
+ * TODO: eliminate this dependency (cvc4-projects #120).
+ */
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+
+/**
+ * This returns the result of checking the satisfiability of formula query.
+ *
+ * If necessary, smte is initialized to the SMT engine that checked its
+ * satisfiability.
+ */
+Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+
+/**
+ * This returns the result of checking the satisfiability of formula query.
+ *
+ * In contrast to above, this is used if the user of this method is not
+ * concerned with the state of the SMT engine after the check.
+ *
+ * @param query The query to check
+ * @param needsTimeout Whether we would like to set a timeout
+ * @param timeout The timeout (in milliseconds)
+ */
+Result checkWithSubsolver(Node query,
+ bool needsTimeout = false,
+ unsigned long timeout = 0);
+
+/**
+ * This returns the result of checking the satisfiability of formula query.
+ * Additionally, if the query is satisfiable, it adds the model values for vars
+ * into modelVars.
+ *
+ * @param query The query to check
+ * @param vars The variables we are interesting in getting a model for.
+ * @param modelVals A vector storing the model values of variables in vars.
+ * @param needsTimeout Whether we would like to set a timeout
+ * @param timeout The timeout (in milliseconds)
+ */
+Result checkWithSubsolver(Node query,
+ const std::vector<Node>& vars,
+ std::vector<Node>& modelVals,
+ bool needsTimeout = false,
+ unsigned long timeout = 0);
+
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H */
projects / cvc5.git / commitdiff