This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:
(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification
The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.
In this PR:
define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
smt/check_models.h
smt/command.cpp
smt/command.h
- smt/defined_function.h
smt/dump.cpp
smt/dump.h
smt/dump_manager.cpp
#include "preprocessing/preprocessing_pass_context.h"
#include "expr/node_algorithm.h"
+#include "smt/env.h"
#include "theory/theory_engine.h"
#include "theory/theory_model.h"
PreprocessingPassContext::PreprocessingPassContext(
SmtEngine* smt,
- theory::booleans::CircuitPropagator* circuitPropagator,
- ProofNodeManager* pnm)
+ Env& env,
+ theory::booleans::CircuitPropagator* circuitPropagator)
: d_smt(smt),
- d_resourceManager(smt->getResourceManager()),
- d_topLevelSubstitutions(smt->getUserContext(), pnm),
+ d_env(env),
d_circuitPropagator(circuitPropagator),
- d_pnm(pnm),
- d_symsInAssertions(smt->getUserContext())
+ d_symsInAssertions(env.getUserContext())
{
}
theory::TrustSubstitutionMap&
PreprocessingPassContext::getTopLevelSubstitutions()
{
- return d_topLevelSubstitutions;
+ return d_env.getTopLevelSubstitutions();
}
+context::Context* PreprocessingPassContext::getUserContext()
+{
+ return d_env.getUserContext();
+}
+context::Context* PreprocessingPassContext::getDecisionContext()
+{
+ return d_env.getContext();
+}
+void PreprocessingPassContext::spendResource(Resource r)
+{
+ d_env.getResourceManager()->spendResource(r);
+}
void PreprocessingPassContext::recordSymbolsInAssertions(
const std::vector<Node>& assertions)
{
const Node& rhs,
ProofGenerator* pg)
{
- d_topLevelSubstitutions.addSubstitution(lhs, rhs, pg);
+ getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg);
+ // also add as a model substitution
+ addModelSubstitution(lhs, rhs);
+}
+
+void PreprocessingPassContext::addSubstitution(const Node& lhs,
+ const Node& rhs,
+ PfRule id,
+ const std::vector<Node>& args)
+{
+ getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args);
// also add as a model substitution
addModelSubstitution(lhs, rhs);
}
ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
{
- return d_pnm;
+ return d_env.getProofNodeManager();
}
} // namespace preprocessing
public:
PreprocessingPassContext(
SmtEngine* smt,
- theory::booleans::CircuitPropagator* circuitPropagator,
- ProofNodeManager* pnm);
+ Env& env,
+ theory::booleans::CircuitPropagator* circuitPropagator);
SmtEngine* getSmt() { return d_smt; }
TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); }
prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); }
- context::Context* getUserContext() { return d_smt->getUserContext(); }
- context::Context* getDecisionContext() { return d_smt->getContext(); }
+ context::Context* getUserContext();
+ context::Context* getDecisionContext();
theory::booleans::CircuitPropagator* getCircuitPropagator()
{
return d_symsInAssertions;
}
- void spendResource(Resource r)
- {
- d_resourceManager->spendResource(r);
- }
+ void spendResource(Resource r);
/** Get the current logic info of the SmtEngine */
const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
void addSubstitution(const Node& lhs,
const Node& rhs,
ProofGenerator* pg = nullptr);
+ /** Same as above, with proof id */
+ void addSubstitution(const Node& lhs,
+ const Node& rhs,
+ PfRule id,
+ const std::vector<Node>& args);
/** The the proof node manager associated with this context, if it exists */
ProofNodeManager* getProofNodeManager();
private:
/** Pointer to the SmtEngine that this context was created in. */
SmtEngine* d_smt;
-
- /** Pointer to the ResourceManager for this context. */
- ResourceManager* d_resourceManager;
-
- /* The top level substitutions */
- theory::TrustSubstitutionMap d_topLevelSubstitutions;
-
+ /** Reference to the environment. */
+ Env& d_env;
/** Instance of the circuit propagator */
theory::booleans::CircuitPropagator* d_circuitPropagator;
- /** Pointer to the proof node manager, if it exists */
- ProofNodeManager* d_pnm;
-
/**
* The (user-context-dependent) set of symbols that occur in at least one
* assertion in the current user context.
#include "options/smt_options.h"
#include "proof/proof_manager.h"
#include "smt/abstract_values.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
+#include "theory/trust_substitutions.h"
using namespace cvc5::theory;
using namespace cvc5::kind;
namespace cvc5 {
namespace smt {
-Assertions::Assertions(context::UserContext* u, AbstractValues& absv)
- : d_userContext(u),
+Assertions::Assertions(Env& env, AbstractValues& absv)
+ : d_env(env),
d_absValues(absv),
- d_assertionList(nullptr),
+ d_produceAssertions(false),
+ d_assertionList(env.getUserContext()),
d_globalNegation(false),
d_assertions()
{
Assertions::~Assertions()
{
- if (d_assertionList != nullptr)
- {
- d_assertionList->deleteSelf();
- }
}
void Assertions::finishInit()
{
// In the case of incremental solving, we appear to need these to
// ensure the relevant Nodes remain live.
- d_assertionList = new (true) AssertionList(d_userContext);
- d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
+ d_produceAssertions = true;
+ d_globalDefineFunLemmas.reset(new std::vector<Node>());
}
}
Node n = d_absValues.substituteAbstractValues(e);
// Ensure expr is type-checked at this point.
ensureBoolean(n);
- addFormula(n, inUnsatCore, true, true, false);
+ addFormula(n, inUnsatCore, true, true, false, false);
}
- if (d_globalDefineFunRecLemmas != nullptr)
+ if (d_globalDefineFunLemmas != nullptr)
{
// Global definitions are asserted at check-sat-time because we have to
// make sure that they are always present (they are essentially level
// zero assertions)
- for (const Node& lemma : *d_globalDefineFunRecLemmas)
+ for (const Node& lemma : *d_globalDefineFunLemmas)
{
- addFormula(lemma, false, true, false, false);
+ addFormula(lemma, false, true, false, true, false);
}
}
}
{
ensureBoolean(n);
bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
- addFormula(n, inUnsatCore, true, false, maybeHasFv);
+ addFormula(n, inUnsatCore, true, false, false, maybeHasFv);
}
std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
context::CDList<Node>* Assertions::getAssertionList()
{
- return d_assertionList;
+ return d_produceAssertions ? &d_assertionList : nullptr;
}
-void Assertions::addFormula(
- TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
+void Assertions::addFormula(TNode n,
+ bool inUnsatCore,
+ bool inInput,
+ bool isAssumption,
+ bool isFunDef,
+ bool maybeHasFv)
{
// add to assertion list if it exists
- if (d_assertionList != nullptr)
+ if (d_produceAssertions)
{
- d_assertionList->push_back(n);
+ d_assertionList.push_back(n);
}
if (n.isConst() && n.getConst<bool>())
{
// true, nothing to do
return;
}
-
Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< "), inUnsatCore = " << inUnsatCore
<< ", inInput = " << inInput
- << ", isAssumption = " << isAssumption << std::endl;
+ << ", isAssumption = " << isAssumption
+ << ", isFunDef = " << isFunDef << std::endl;
+ if (isFunDef)
+ {
+ // if a non-recursive define-fun, just add as a top-level substitution
+ if (n.getKind() == EQUAL && n[0].isVar())
+ {
+ // A define-fun is an assumption in the overall proof, thus
+ // we justify the substitution with ASSUME here.
+ d_env.getTopLevelSubstitutions().addSubstitution(
+ n[0], n[1], PfRule::ASSUME, {}, {n});
+ return;
+ }
+ }
// Ensure that it does not contain free variables
if (maybeHasFv)
d_assertions.push_back(n, isAssumption, true);
}
-void Assertions::addDefineFunRecDefinition(Node n, bool global)
+void Assertions::addDefineFunDefinition(Node n, bool global)
{
n = d_absValues.substituteAbstractValues(n);
- if (d_assertionList != nullptr)
- {
- d_assertionList->push_back(n);
- }
- if (global && d_globalDefineFunRecLemmas != nullptr)
+ if (global && d_globalDefineFunLemmas != nullptr)
{
// Global definitions are asserted at check-sat-time because we have to
// make sure that they are always present
Assert(!language::isInputLangSygus(options::inputLanguage()));
- d_globalDefineFunRecLemmas->emplace_back(n);
+ d_globalDefineFunLemmas->emplace_back(n);
}
else
{
- bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
- addFormula(n, false, true, false, maybeHasFv);
+ // we don't check for free variables here, since even if we are sygus,
+ // we could contain functions-to-synthesize within definitions.
+ addFormula(n, false, true, false, true, false);
}
}
#include "preprocessing/assertion_pipeline.h"
namespace cvc5 {
+
+class Env;
+
namespace smt {
class AbstractValues;
typedef context::CDList<Node> AssertionList;
public:
- Assertions(context::UserContext* u, AbstractValues& absv);
+ Assertions(Env& env, AbstractValues& absv);
~Assertions();
/**
* Finish initialization, called once after options are finalized. Sets up
*/
void assertFormula(const Node& n, bool inUnsatCore = true);
/**
- * Assert that n corresponds to an assertion from a define-fun-rec command.
+ * Assert that n corresponds to an assertion from a define-fun or
+ * define-fun-rec command.
* This assertion is added to the set of assertions maintained by this class.
* If this has a global definition, this assertion is persistent for any
* subsequent check-sat calls.
*/
- void addDefineFunRecDefinition(Node n, bool global);
+ void addDefineFunDefinition(Node n, bool global);
/**
* Get the assertions pipeline, which contains the set of assertions we are
* currently processing.
bool inUnsatCore,
bool inInput,
bool isAssumption,
+ bool isFunDef,
bool maybeHasFv);
- /** pointer to the user context */
- context::UserContext* d_userContext;
+ /** Reference to the environment. */
+ Env& d_env;
/** Reference to the abstract values utility */
AbstractValues& d_absValues;
+ /** Whether we are producing assertions */
+ bool d_produceAssertions;
/**
* The assertion list (before any conversion) for supporting
* getAssertions(). Only maintained if in incremental mode.
*/
- AssertionList* d_assertionList;
+ AssertionList d_assertionList;
/**
- * List of lemmas generated for global recursive function definitions. We
+ * List of lemmas generated for global (recursive) function definitions. We
* assert this list of definitions in each check-sat call.
*/
- std::unique_ptr<std::vector<Node>> d_globalDefineFunRecLemmas;
+ std::unique_ptr<std::vector<Node>> d_globalDefineFunLemmas;
/**
* The list of assumptions from the previous call to checkSatisfiability.
* Note that if the last call to checkSatisfiability was an entailment check,
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Defined function data structure.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SMT__DEFINED_FUNCTION_H
-#define CVC5__SMT__DEFINED_FUNCTION_H
-
-#include <vector>
-
-#include "expr/node.h"
-
-namespace cvc5 {
-namespace smt {
-
-/**
- * Representation of a defined function. We keep these around in
- * SmtEngine to permit expanding definitions late (and lazily), to
- * support getValue() over defined functions, to support user output
- * in terms of defined functions, etc.
- */
-class DefinedFunction
-{
- public:
- DefinedFunction() {}
- DefinedFunction(Node func, const std::vector<Node>& formals, Node formula)
- : d_func(func), d_formals(formals), d_formula(formula)
- {
- }
- /** get the function */
- Node getFunction() const { return d_func; }
- /** get the formal argument list of the function */
- const std::vector<Node>& getFormals() const { return d_formals; }
- /** get the formula that defines it */
- Node getFormula() const { return d_formula; }
-
- private:
- /** the function */
- Node d_func;
- /** the formal argument list */
- std::vector<Node> d_formals;
- /** the formula */
- Node d_formula;
-}; /* class DefinedFunction */
-
-} // namespace smt
-} // namespace cvc5
-
-#endif /* CVC5__SMT__DEFINED_FUNCTION_H */
#include "smt/dump_manager.h"
#include "smt/smt_engine_stats.h"
#include "theory/rewriter.h"
+#include "theory/trust_substitutions.h"
#include "util/resource_manager.h"
#include "util/statistics_registry.h"
d_nodeManager(nm),
d_proofNodeManager(nullptr),
d_rewriter(new theory::Rewriter()),
+ d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())),
d_dumpManager(new DumpManager(d_userContext.get())),
d_logic(),
d_statisticsRegistry(std::make_unique<StatisticsRegistry>()),
void Env::setProofNodeManager(ProofNodeManager* pnm)
{
+ Assert(pnm != nullptr);
+ Assert(d_proofNodeManager == nullptr);
d_proofNodeManager = pnm;
d_rewriter->setProofNodeManager(pnm);
+ d_topLevelSubs->setProofNodeManager(pnm);
}
void Env::shutdown()
theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
+theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()
+{
+ return *d_topLevelSubs.get();
+}
+
DumpManager* Env::getDumpManager() { return d_dumpManager.get(); }
const LogicInfo& Env::getLogicInfo() const { return d_logic; }
namespace theory {
class Rewriter;
+class TrustSubstitutionMap;
}
/**
/** Get a pointer to the Rewriter owned by this Env. */
theory::Rewriter* getRewriter();
+ /** Get a reference to the top-level substitution map */
+ theory::TrustSubstitutionMap& getTopLevelSubstitutions();
+
/** Get a pointer to the underlying dump manager. */
smt::DumpManager* getDumpManager();
private:
/* Private initialization ------------------------------------------------- */
- /** Set the statistics registry */
- void setStatisticsRegistry(StatisticsRegistry* statReg);
/** Set proof node manager if it exists */
void setProofNodeManager(ProofNodeManager* pnm);
* specific to an SmtEngine/TheoryEngine instance.
*/
std::unique_ptr<theory::Rewriter> d_rewriter;
+ /** The top level substitutions */
+ std::unique_ptr<theory::TrustSubstitutionMap> d_topLevelSubs;
/** The dump manager */
std::unique_ptr<smt::DumpManager> d_dumpManager;
/**
#include "expr/node_manager_attributes.h"
#include "preprocessing/assertion_pipeline.h"
-#include "smt/defined_function.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_stats.h"
#include "theory/theory_engine.h"
namespace cvc5 {
namespace smt {
-ExpandDefs::ExpandDefs(SmtEngine& smt,
- ResourceManager& rm,
- SmtEngineStatistics& stats)
- : d_smt(smt), d_resourceManager(rm), d_smtStats(stats), d_tpg(nullptr)
+ExpandDefs::ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats)
+ : d_smt(smt), d_env(env), d_smtStats(stats), d_tpg(nullptr)
{
}
TConvProofGenerator* tpg)
{
const TNode orig = n;
- NodeManager* nm = d_smt.getNodeManager();
std::stack<std::tuple<Node, Node, bool>> worklist;
std::stack<Node> result;
worklist.push(std::make_tuple(Node(n), Node(n), false));
do
{
- d_resourceManager.spendResource(Resource::PreprocessStep);
+ d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
// n is the input / original
// node is the output / result
// Working downwards
if (!childrenPushed)
{
- Kind k = n.getKind();
-
// we can short circuit (variable) leaves
if (n.isVar())
{
- SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
- SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n);
- if (i != dfuns->end())
- {
- Node f = (*i).second.getFormula();
- const std::vector<Node>& formals = (*i).second.getFormals();
- // replacement must be closed
- if (!formals.empty())
- {
- f = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, formals), f);
- }
- // are we are producing proofs for this call?
- if (tpg != nullptr)
- {
- // if this is a variable, we can simply assume it
- // ------- ASSUME
- // n = f
- Node conc = n.eqNode(f);
- tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}, true);
- }
- // must recursively expand its definition
- TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg);
- Node fe = tfe.isNull() ? f : tfe.getNode();
- // don't bother putting in the cache
- result.push(fe);
- continue;
- }
// don't bother putting in the cache
result.push(n);
continue;
result.push(ret.isNull() ? n : ret);
continue;
}
-
- // otherwise expand it
- bool doExpand = false;
- if (k == APPLY_UF)
- {
- // Always do beta-reduction here. The reason is that there may be
- // operators such as INTS_MODULUS in the body of the lambda that would
- // otherwise be introduced by beta-reduction via the rewriter, but are
- // not expanded here since the traversal in this function does not
- // traverse the operators of nodes. Hence, we beta-reduce here to
- // ensure terms in the body of the lambda are expanded during this
- // call.
- if (n.getOperator().getKind() == LAMBDA)
- {
- doExpand = true;
- }
- else
- {
- // We always check if this operator corresponds to a defined function.
- doExpand = d_smt.isDefinedFunction(n.getOperator());
- }
- }
- // the premise of the proof of expansion (if we are expanding a definition
- // and proofs are enabled)
- std::vector<Node> pfExpChildren;
- if (doExpand)
- {
- std::vector<Node> formals;
- TNode fm;
- if (n.getOperator().getKind() == LAMBDA)
- {
- TNode op = n.getOperator();
- // lambda
- for (unsigned i = 0; i < op[0].getNumChildren(); i++)
- {
- formals.push_back(op[0][i]);
- }
- fm = op[1];
- }
- else
- {
- // application of a user-defined symbol
- TNode func = n.getOperator();
- SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
- SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func);
- if (i == dfuns->end())
- {
- throw TypeCheckingExceptionPrivate(
- n,
- std::string("Undefined function: `") + func.toString() + "'");
- }
- DefinedFunction def = (*i).second;
- formals = def.getFormals();
-
- if (Debug.isOn("expand"))
- {
- Debug("expand") << "found: " << n << std::endl;
- Debug("expand") << " func: " << func << std::endl;
- std::string name = func.getAttribute(expr::VarNameAttr());
- Debug("expand") << " : \"" << name << "\"" << std::endl;
- }
- if (Debug.isOn("expand"))
- {
- Debug("expand") << " defn: " << def.getFunction() << std::endl
- << " [";
- if (formals.size() > 0)
- {
- copy(formals.begin(),
- formals.end() - 1,
- std::ostream_iterator<Node>(Debug("expand"), ", "));
- Debug("expand") << formals.back();
- }
- Debug("expand")
- << "]" << std::endl
- << " " << def.getFunction().getType() << std::endl
- << " " << def.getFormula() << std::endl;
- }
-
- fm = def.getFormula();
- // are we producing proofs for this call?
- if (tpg != nullptr)
- {
- Node pfRhs = fm;
- if (!formals.empty())
- {
- Node bvl = nm->mkNode(BOUND_VAR_LIST, formals);
- pfRhs = nm->mkNode(LAMBDA, bvl, pfRhs);
- }
- Assert(func.getType().isComparableTo(pfRhs.getType()));
- pfExpChildren.push_back(func.eqNode(pfRhs));
- }
- }
-
- Node instance = fm.substitute(formals.begin(),
- formals.end(),
- n.begin(),
- n.begin() + formals.size());
- Debug("expand") << "made : " << instance << std::endl;
- // are we producing proofs for this call?
- if (tpg != nullptr)
- {
- if (n != instance)
- {
- // This code is run both when we are doing expand definitions and
- // simple beta reduction.
- //
- // f = (lambda ((x T)) t) [if we are expanding a definition]
- // ---------------------- MACRO_SR_PRED_INTRO
- // n = instance
- Node conc = n.eqNode(instance);
- tpg->addRewriteStep(n,
- instance,
- PfRule::MACRO_SR_PRED_INTRO,
- pfExpChildren,
- {conc},
- true);
- }
- }
- // now, call expand definitions again on the result
- TrustNode texp = expandDefinitions(instance, cache, expandOnly, tpg);
- Node expanded = texp.isNull() ? instance : texp.getNode();
- cache[n] = n == expanded ? Node::null() : expanded;
- result.push(expanded);
- continue;
- }
- else if (!expandOnly)
+ if (!expandOnly)
{
// do not do any theory stuff if expandOnly is true
return TrustNode::mkTrustRewrite(orig, res, tpg);
}
-void ExpandDefs::expandAssertions(AssertionPipeline& assertions,
- bool expandOnly)
-{
- Chat() << "expanding definitions in assertions..." << std::endl;
- Trace("exp-defs") << "ExpandDefs::simplify(): expanding definitions"
- << std::endl;
- TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime);
- std::unordered_map<Node, Node, NodeHashFunction> cache;
- for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
- {
- Node assert = assertions[i];
- // notice we call this method with only one value of expandOnly currently,
- // hence we maintain only a single set of proof steps in d_tpg.
- TrustNode expd = expandDefinitions(assert, cache, expandOnly, d_tpg.get());
- if (!expd.isNull())
- {
- Trace("exp-defs") << "ExpandDefs::expandAssertions: " << assert << " -> "
- << expd.getNode() << std::endl;
- assertions.replaceTrusted(i, expd);
- }
- }
-}
-
void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm)
{
if (d_tpg == nullptr)
{
d_tpg.reset(new TConvProofGenerator(pnm,
- d_smt.getUserContext(),
+ d_env.getUserContext(),
TConvPolicy::FIXPOINT,
TConvCachePolicy::NEVER,
"ExpandDefs::TConvProofGenerator",
namespace cvc5 {
+class Env;
class ProofNodeManager;
-class ResourceManager;
class SmtEngine;
class TConvProofGenerator;
class ExpandDefs
{
public:
- ExpandDefs(SmtEngine& smt, ResourceManager& rm, SmtEngineStatistics& stats);
+ ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats);
~ExpandDefs();
/**
* Expand definitions in term n. Return the expanded form of n.
TNode n,
std::unordered_map<Node, Node, NodeHashFunction>& cache,
bool expandOnly = false);
- /**
- * Expand defintitions in assertions. This applies this above method to each
- * assertion in the given pipeline.
- */
- void expandAssertions(preprocessing::AssertionPipeline& assertions,
- bool expandOnly = false);
/**
* Set proof node manager, which signals this class to enable proofs using the
TConvProofGenerator* tpg);
/** Reference to the SMT engine */
SmtEngine& d_smt;
- /** Reference to resource manager */
- ResourceManager& d_resourceManager;
+ /** Reference to the environment. */
+ Env& d_env;
/** Reference to the SMT stats */
SmtEngineStatistics& d_smtStats;
/** A proof generator for the term conversion. */
#include "smt/abstract_values.h"
#include "smt/assertions.h"
#include "smt/dump.h"
+#include "smt/env.h"
#include "smt/preprocess_proof_generator.h"
#include "smt/smt_engine.h"
+#include "theory/rewriter.h"
using namespace std;
using namespace cvc5::theory;
namespace smt {
Preprocessor::Preprocessor(SmtEngine& smt,
- context::UserContext* u,
+ Env& env,
AbstractValues& abs,
SmtEngineStatistics& stats)
- : d_context(u),
- d_smt(smt),
+ : d_smt(smt),
+ d_env(env),
d_absValues(abs),
d_propagator(true, true),
- d_assertionsProcessed(u, false),
- d_exDefs(smt, *smt.getResourceManager(), stats),
- d_processor(smt, d_exDefs, *smt.getResourceManager(), stats),
+ d_assertionsProcessed(env.getUserContext(), false),
+ d_exDefs(smt, d_env, stats),
+ d_processor(smt, *smt.getResourceManager(), stats),
d_pnm(nullptr)
{
}
void Preprocessor::finishInit()
{
d_ppContext.reset(new preprocessing::PreprocessingPassContext(
- &d_smt, &d_propagator, d_pnm));
+ &d_smt, d_env, &d_propagator));
// initialize the preprocessing passes
d_processor.finishInit(d_ppContext.get());
Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly)
{
std::unordered_map<Node, Node, NodeHashFunction> cache;
- return d_exDefs.expandDefinitions(n, cache, expandOnly);
+ return expandDefinitions(n, cache, expandOnly);
}
Node Preprocessor::expandDefinitions(
// Ensure node is type-checked at this point.
n.getType(true);
}
- // expand only = true
- return d_exDefs.expandDefinitions(n, cache, expandOnly);
+ // we apply substitutions here, before expanding definitions
+ theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
+ n = sm.apply(n);
+ if (!expandOnly)
+ {
+ // expand only = true
+ n = d_exDefs.expandDefinitions(n, cache, expandOnly);
+ }
+ return n;
}
Node Preprocessor::simplify(const Node& node)
d_smt.getOutputManager().getPrinter().toStreamCmdSimplify(
d_smt.getOutputManager().getDumpOut(), node);
}
- Node nas = d_absValues.substituteAbstractValues(node);
- if (options::typeChecking())
- {
- // ensure node is type-checked at this point
- nas.getType(true);
- }
std::unordered_map<Node, Node, NodeHashFunction> cache;
- Node n = d_exDefs.expandDefinitions(nas, cache);
- TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n);
- Node ns = ts.isNull() ? n : ts.getNode();
- return ns;
+ Node ret = expandDefinitions(node, cache, false);
+ ret = theory::Rewriter::rewrite(ret);
+ return ret;
}
void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
Assert(pppg != nullptr);
d_pnm = pppg->getManager();
d_exDefs.setProofNodeManager(d_pnm);
- d_propagator.setProof(d_pnm, d_context, pppg);
+ d_propagator.setProof(d_pnm, d_env.getUserContext(), pppg);
}
} // namespace smt
#include "theory/booleans/circuit_propagator.h"
namespace cvc5 {
+class Env;
namespace preprocessing {
class PreprocessingPassContext;
}
{
public:
Preprocessor(SmtEngine& smt,
- context::UserContext* u,
+ Env& env,
AbstractValues& abs,
SmtEngineStatistics& stats);
~Preprocessor();
const Node& n,
std::unordered_map<Node, Node, NodeHashFunction>& cache,
bool expandOnly = false);
-
/**
* Set proof node manager. Enables proofs in this preprocessor.
*/
void setProofGenerator(PreprocessProofGenerator* pppg);
private:
- /** A copy of the current context */
- context::Context* d_context;
/** Reference to the parent SmtEngine */
SmtEngine& d_smt;
+ /** Reference to the env */
+ Env& d_env;
/** Reference to the abstract values utility */
AbstractValues& d_absValues;
/**
#include "preprocessing/preprocessing_pass_registry.h"
#include "printer/printer.h"
#include "smt/assertions.h"
-#include "smt/defined_function.h"
#include "smt/dump.h"
#include "smt/expand_definitions.h"
#include "smt/smt_engine.h"
};
ProcessAssertions::ProcessAssertions(SmtEngine& smt,
- ExpandDefs& exDefs,
ResourceManager& rm,
SmtEngineStatistics& stats)
: d_smt(smt),
- d_exDefs(exDefs),
d_resourceManager(rm),
d_smtStats(stats),
d_preprocessingPassContext(nullptr)
<< "ProcessAssertions::processAssertions() : pre-definition-expansion"
<< endl;
dumpAssertions("pre-definition-expansion", assertions);
- // Expand definitions, which replaces defined functions with their definition
- // and does beta reduction. Notice we pass true as the second argument since
- // we do not want to call theories to expand definitions here, since we want
+ // Apply substitutions first. If we are non-incremental, this has only the
+ // effect of replacing defined functions with their definitions.
+ // We do not call theory-specific expand definitions here, since we want
// to give the opportunity to rewrite/preprocess terms before expansion.
- d_exDefs.expandAssertions(assertions, true);
+ d_passes["apply-substs"]->apply(&assertions);
Trace("smt-proc")
<< "ProcessAssertions::processAssertions() : post-definition-expansion"
<< endl;
namespace smt {
class Assertions;
-class ExpandDefs;
struct SmtEngineStatistics;
/**
public:
ProcessAssertions(SmtEngine& smt,
- ExpandDefs& exDefs,
ResourceManager& rm,
SmtEngineStatistics& stats);
~ProcessAssertions();
private:
/** Reference to the SMT engine */
SmtEngine& d_smt;
- /** Reference to expand definitions module */
- ExpandDefs& d_exDefs;
/** Reference to resource manager */
ResourceManager& d_resourceManager;
/** Reference to the SMT stats */
#include "options/smt_options.h"
#include "proof/dot/dot_printer.h"
#include "smt/assertions.h"
-#include "smt/defined_function.h"
#include "smt/preprocess_proof_generator.h"
#include "smt/proof_post_processor.h"
PfManager::~PfManager() {}
-void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
- Assertions& as,
- DefinedFunctionMap& df)
+void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
{
// Note this assumes that setFinalProof is only called once per unsat
// response. This method would need to cache its result otherwise.
}
std::vector<Node> assertions;
- getAssertions(as, df, assertions);
+ getAssertions(as, assertions);
if (Trace.isOn("smt-proof"))
{
void PfManager::printProof(std::ostream& out,
std::shared_ptr<ProofNode> pfn,
- Assertions& as,
- DefinedFunctionMap& df)
+ Assertions& as)
{
Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
- std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
+ std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as);
// if we are in incremental mode, we don't want to invalidate the proof
// nodes in fp, since these may be reused in further check-sat calls
if (options::incrementalSolving()
out << "\n)\n";
}
}
-void PfManager::checkProof(std::shared_ptr<ProofNode> pfn,
- Assertions& as,
- DefinedFunctionMap& df)
+void PfManager::checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
{
Trace("smt-proof") << "PfManager::checkProof: start" << std::endl;
- std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
+ std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as);
Trace("smt-proof-debug") << "PfManager::checkProof: returned " << *fp.get()
<< std::endl;
}
}
std::shared_ptr<ProofNode> PfManager::getFinalProof(
- std::shared_ptr<ProofNode> pfn, Assertions& as, DefinedFunctionMap& df)
+ std::shared_ptr<ProofNode> pfn, Assertions& as)
{
- setFinalProof(pfn, as, df);
+ setFinalProof(pfn, as);
Assert(d_finalProof);
return d_finalProof;
}
void PfManager::getAssertions(Assertions& as,
- DefinedFunctionMap& df,
std::vector<Node>& assertions)
{
context::CDList<Node>* al = as.getAssertionList();
{
assertions.push_back(*i);
}
- NodeManager* nm = NodeManager::currentNM();
- for (const std::pair<const Node, const smt::DefinedFunction>& dfn : df)
- {
- Node def = dfn.second.getFormula();
- const std::vector<Node>& formals = dfn.second.getFormals();
- if (!formals.empty())
- {
- Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, formals);
- def = nm->mkNode(kind::LAMBDA, bvl, def);
- }
- // assume the (possibly higher order) equality
- Node eq = dfn.first.eqNode(def);
- assertions.push_back(eq);
- }
}
} // namespace smt
namespace smt {
class Assertions;
-class DefinedFunction;
class PreprocessProofGenerator;
class ProofPostproccess;
*/
class PfManager
{
- /** The type of our internal map of defined functions */
- using DefinedFunctionMap =
- context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
-
public:
PfManager(context::UserContext* u, SmtEngine* smte);
~PfManager();
* The argument pfn is the proof for false in the current context.
*
* Throws an assertion failure if pg cannot provide a closed proof with
- * respect to assertions in as and df. For the latter, entries in the defined
- * function map correspond to equalities of the form (= f (lambda (...) t)),
- * which are considered assertions in the final proof.
+ * respect to assertions in as. Note this includes equalities of the form
+ * (= f (lambda (...) t)) which originate from define-fun commands for f.
+ * These are considered assertions in the final proof.
*/
void printProof(std::ostream& out,
std::shared_ptr<ProofNode> pfn,
- Assertions& as,
- DefinedFunctionMap& df);
+ Assertions& as);
/**
* Check proof, same as above, without printing.
*/
- void checkProof(std::shared_ptr<ProofNode> pfn,
- Assertions& as,
- DefinedFunctionMap& df);
+ void checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
/**
* Get final proof.
* The argument pfn is the proof for false in the current context.
*/
std::shared_ptr<ProofNode> getFinalProof(std::shared_ptr<ProofNode> pfn,
- Assertions& as,
- DefinedFunctionMap& df);
+ Assertions& as);
//--------------------------- access to utilities
/** Get a pointer to the ProofChecker owned by this. */
ProofChecker* getProofChecker() const;
* Set final proof, which initializes d_finalProof to the given proof node of
* false, postprocesses it, and stores it in d_finalProof.
*/
- void setFinalProof(std::shared_ptr<ProofNode> pfn,
- Assertions& as,
- DefinedFunctionMap& df);
+ void setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
/**
* Get assertions from the assertions
*/
void getAssertions(Assertions& as,
- DefinedFunctionMap& df,
std::vector<Node>& assertions);
/** The false node */
Node d_false;
#include "smt/abstract_values.h"
#include "smt/assertions.h"
#include "smt/check_models.h"
-#include "smt/defined_function.h"
#include "smt/dump.h"
#include "smt/dump_manager.h"
#include "smt/env.h"
: d_env(new Env(nm, optr)),
d_state(new SmtEngineState(getContext(), getUserContext(), *this)),
d_absValues(new AbstractValues(getNodeManager())),
- d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
+ d_asserts(new Assertions(*d_env.get(), *d_absValues.get())),
d_routListener(new ResourceOutListener(*this)),
d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
d_smtSolver(nullptr),
d_checkModels(nullptr),
d_pfManager(nullptr),
d_ucManager(nullptr),
- d_definedFunctions(nullptr),
d_sygusSolver(nullptr),
d_abductSolver(nullptr),
d_interpolSolver(nullptr),
// make statistics
d_stats.reset(new SmtEngineStatistics());
// reset the preprocessor
- d_pp.reset(new smt::Preprocessor(
- *this, getUserContext(), *d_absValues.get(), *d_stats));
+ d_pp.reset(
+ new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats));
// make the SMT solver
d_smtSolver.reset(
new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats));
// being parsed from the input file. Because of this, we cannot trust
// that d_env->getOption(options::unsatCores) is set correctly yet.
d_proofManager.reset(new ProofManager(getUserContext()));
-
- d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
}
bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); }
// of context-dependent data structures
d_state->cleanup();
- d_definedFunctions->deleteSelf();
-
//destroy all passes before destroying things that they refer to
d_pp->cleanup();
ss << language::SetLanguage(
language::SetLanguage::getLanguage(Dump.getStream()))
<< func;
- std::vector<Node> nFormals;
- nFormals.reserve(formals.size());
- for (const Node& formal : formals)
- {
- nFormals.push_back(formal);
- }
-
- DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula);
+ DefineFunctionNodeCommand nc(ss.str(), func, formals, formula);
getDumpManager()->addToDump(nc, "declarations");
// type check body
debugCheckFunctionBody(formula, formals, func);
// Substitute out any abstract values in formula
- Node formNode = d_absValues->substituteAbstractValues(formula);
- DefinedFunction def(func, formals, formNode);
- // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
- // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
- // d_haveAdditions = true;
- Debug("smt") << "definedFunctions insert " << func << " " << formNode << endl;
-
- if (global)
- {
- d_definedFunctions->insertAtContextLevelZero(func, def);
- }
- else
+ Node def = d_absValues->substituteAbstractValues(formula);
+ if (!formals.empty())
{
- d_definedFunctions->insert(func, def);
+ NodeManager* nm = NodeManager::currentNM();
+ def = nm->mkNode(
+ kind::LAMBDA, nm->mkNode(kind::BOUND_VAR_LIST, formals), def);
}
+ // A define-fun is treated as a (higher-order) assertion. It is provided
+ // to the assertions object. It will be added as a top-level substitution
+ // within this class, possibly multiple times if global is true.
+ Node feq = func.eqNode(def);
+ d_asserts->addDefineFunDefinition(feq, global);
}
void SmtEngine::defineFunctionsRec(
// notice we don't call assertFormula directly, since this would
// duplicate the output on raw-benchmark.
// add define recursive definition to the assertions
- d_asserts->addDefineFunRecDefinition(lem, global);
+ d_asserts->addDefineFunDefinition(lem, global);
}
}
defineFunctionsRec(funcs, formals_multi, formulas, global);
}
-bool SmtEngine::isDefinedFunction(Node func)
-{
- Debug("smt") << "isDefined function " << func << "?" << std::endl;
- return d_definedFunctions->find(func) != d_definedFunctions->end();
-}
-
Result SmtEngine::quickCheck() {
Assert(d_state->isFullyInited());
Trace("smt") << "SMT quickCheck()" << endl;
ModelBlocker::getModelBlocker(eassertsProc,
m->getTheoryModel(),
d_env->getOption(options::blockModelsMode));
+ Trace("smt") << "Block formula: " << eblocker << std::endl;
return assertFormula(eblocker);
}
std::shared_ptr<ProofNode> pePfn = pe->getProof();
if (d_env->getOption(options::checkProofs))
{
- d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
+ d_pfManager->checkProof(pePfn, *d_asserts);
}
}
pepf = pe->getProof();
}
Assert(pepf != nullptr);
- std::shared_ptr<ProofNode> pfn =
- d_pfManager->getFinalProof(pepf, *d_asserts, *d_definedFunctions);
+ std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts);
std::vector<Node> core;
d_ucManager->getUnsatCore(pfn, *d_asserts, core);
return UnsatCore(core);
PropEngine* pe = getPropEngine();
Assert(pe != nullptr);
Assert(pe->getProof() != nullptr);
- std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
- pe->getProof(), *d_asserts, *d_definedFunctions);
+ std::shared_ptr<ProofNode> pfn =
+ d_pfManager->getFinalProof(pe->getProof(), *d_asserts);
d_ucManager->getRelevantInstantiations(pfn, insts);
}
Assert(pe->getProof() != nullptr);
Assert(d_pfManager);
std::ostringstream ss;
- d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions);
+ d_pfManager->printProof(ss, pe->getProof(), *d_asserts);
return ss.str();
}
class AbductionSolver;
class InterpolationSolver;
class QuantElimSolver;
-/**
- * Representation of a defined function. We keep these around in
- * SmtEngine to permit expanding definitions late (and lazily), to
- * support getValue() over defined functions, to support user output
- * in terms of defined functions, etc.
- */
-class DefinedFunction;
struct SmtEngineStatistics;
class SmtScope;
Node formula,
bool global = false);
- /** Return true if given expression is a defined function. */
- bool isDefinedFunction(Node func);
-
/**
* Define functions recursive
*
/** Get a pointer to the Rewriter owned by this SmtEngine. */
theory::Rewriter* getRewriter();
-
- /** The type of our internal map of defined functions */
- using DefinedFunctionMap =
- context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
-
- /** Get the defined function map */
- DefinedFunctionMap* getDefinedFunctionMap() { return d_definedFunctions; }
/**
* Get expanded assertions.
*
* from refutations. */
std::unique_ptr<smt::UnsatCoreManager> d_ucManager;
- /** An index of our defined functions */
- DefinedFunctionMap* d_definedFunctions;
-
/** The solver for sygus queries */
std::unique_ptr<smt::SygusSolver> d_sygusSolver;
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_utils.h"
#include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
#include "theory/smt_engine_subsolver.h"
using namespace cvc5::theory;
// definitions that were added as assertions to the sygus problem.
for (Node a : auxAssertions)
{
- solChecker->assertFormula(a);
+ // We require rewriting here, e.g. so that define-fun from the original
+ // problem are rewritten to true. If this is not the case, then the
+ // assertions module of the subsolver will complain about assertions
+ // with free variables.
+ Node ar = theory::Rewriter::rewrite(a);
+ solChecker->assertFormula(ar);
}
Result r = solChecker->checkSat();
Notice() << "SygusSolver::checkSynthSolution(): result is " << r
MethodId ids)
: d_ctx(c),
d_subs(c),
- d_pnm(pnm),
d_tsubs(c),
- d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr),
- d_subsPg(
- pnm ? new LazyCDProof(pnm, nullptr, c, "TrustSubstitutionMap::subsPg")
- : nullptr),
- d_applyPg(pnm ? new LazyCDProof(
- pnm, nullptr, c, "TrustSubstitutionMap::applyPg")
- : nullptr),
- d_helperPf(pnm, c),
+ d_tspb(nullptr),
+ d_subsPg(nullptr),
+ d_applyPg(nullptr),
+ d_helperPf(nullptr),
d_name(name),
d_trustId(trustId),
d_ids(ids),
d_eqtIndex(c)
{
+ setProofNodeManager(pnm);
+}
+
+void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm)
+{
+ if (pnm != nullptr)
+ {
+ // should not set the proof node manager more than once
+ Assert(d_tspb == nullptr);
+ d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())),
+ d_subsPg.reset(new LazyCDProof(
+ pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg"));
+ d_applyPg.reset(
+ new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg"));
+ d_helperPf.reset(new CDProofSet<LazyCDProof>(pnm, d_ctx));
+ }
}
void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
addSubstitution(x, t, nullptr);
return;
}
- LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx);
+ LazyCDProof* stepPg = d_helperPf->allocateProof(nullptr, d_ctx);
Node eq = x.eqNode(t);
stepPg->addStep(eq, id, children, args);
addSubstitution(x, t, stepPg);
Trace("trust-subs") << "...use generator directly" << std::endl;
return tn.getGenerator();
}
- LazyCDProof* solvePg = d_helperPf.allocateProof(nullptr, d_ctx);
+ LazyCDProof* solvePg = d_helperPf->allocateProof(nullptr, d_ctx);
// Try to transform tn.getProven() to (= x t) here, if necessary
if (!d_tspb->applyPredTransform(proven, eq, {}))
{
public:
TrustSubstitutionMap(context::Context* c,
- ProofNodeManager* pnm,
+ ProofNodeManager* pnm = nullptr,
std::string name = "TrustSubstitutionMap",
PfRule trustId = PfRule::PREPROCESS_LEMMA,
MethodId ids = MethodId::SB_DEFAULT);
+ /** Set proof node manager */
+ void setProofNodeManager(ProofNodeManager* pnm);
/** Gets a reference to the underlying substitution map */
SubstitutionMap& get();
/**
context::Context* d_ctx;
/** The substitution map */
SubstitutionMap d_subs;
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** A context-dependent list of trust nodes */
context::CDList<TrustNode> d_tsubs;
/** Theory proof step buffer */
/**
* A context-dependent list of LazyCDProof, allocated for internal steps.
*/
- CDProofSet<LazyCDProof> d_helperPf;
+ std::unique_ptr<CDProofSet<LazyCDProof>> d_helperPf;
/** Name for debugging */
std::string d_name;
/**
-; COMMAND-LINE: --finite-model-find --fmf-bound-int
+; COMMAND-LINE: --finite-model-find --fmf-bound-int -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
; COMMAND-LINE: --incremental --produce-models --block-models=values
; EXPECT: sat
; EXPECT: sat
-; EXPECT: sat
+; if we only block models restricted to (a,b), then there are only 2 models
+; EXPECT: unsat
(set-logic QF_UFLIA)
(declare-fun a () Int)
(declare-fun b () Int)
-; COMMAND-LINE: --cegqi-bv
+; COMMAND-LINE: --cegqi-bv -q
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --fmf-fun-rlv --sygus-inference
+; COMMAND-LINE: --fmf-fun-rlv --sygus-inference --no-check-models
; EXPECT: sat
(set-logic QF_NRA)
(declare-fun a () Real)
projects / cvc5.git / commitdiff