This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.
The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.
There is no reason to have these two things be separate.
<< "unexpected solution from arith's ppAssert()";
Assert(nullMap.empty())
<< "unexpected substitution from arith's ppAssert()";
- d_preprocContext->addModelSubstitution(*ii, newVar.eqNode(one));
newVars.push_back(newVar);
varRef = newVar;
}
<< "non-clausal preprocessed: " << assertion << std::endl;
}
- // add substitutions to model, or as assertions if needed (when incremental)
- NodeManager* nm = NodeManager::currentNM();
- for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos)
+ // If necessary, add as assertions if needed (when incremental). This is
+ // necessary because certain variables cannot truly be eliminated when
+ // we are in incremental mode. For example, say our first call to check-sat
+ // is a formula F containing variable x. On the second call to check-sat,
+ // say we solve a top-level assertion (= x t). Since the solver already has
+ // constraints involving x, we must still keep (= x t) as an assertion.
+ // However, notice that we do not retract the substitution { x -> t }. This
+ // means that all *subsequent* assertions after (= x t) will replace x by t.
+ if (assertionsToPreprocess->storeSubstsInAsserts())
{
- Node lhs = (*pos).first;
- TrustNode trhs = newSubstitutions->applyTrusted((*pos).second);
- Node rhs = trhs.isNull() ? (*pos).second : trhs.getNode();
- // If using incremental, we must check whether this variable has occurred
- // before now. If it hasn't we can add this as a substitution.
- if (!assertionsToPreprocess->storeSubstsInAsserts()
- || d_preprocContext->getSymsInAssertions().find(lhs)
- == d_preprocContext->getSymsInAssertions().end())
+ for (const std::pair<const Node, const Node>& pos: nss)
{
- Trace("non-clausal-simplify")
- << "substitute: " << lhs << " " << rhs << std::endl;
- d_preprocContext->addModelSubstitution(lhs, rhs);
- }
- else
- {
- // if it has, the substitution becomes an assertion
- Node eq = nm->mkNode(kind::EQUAL, lhs, rhs);
- Trace("non-clausal-simplify")
- << "substitute: will notify SAT layer of substitution: " << eq
- << std::endl;
- trhs = newSubstitutions->applyTrusted((*pos).first);
- Assert(!trhs.isNull());
- assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
- trhs.getGenerator());
+ Node lhs = pos.first;
+ // If using incremental, we must check whether this variable has occurred
+ // before now. If it has, we must add as an assertion.
+ if (d_preprocContext->getSymsInAssertions().contains(lhs))
+ {
+ // if it has, the substitution becomes an assertion
+ TrustNode trhs = newSubstitutions->applyTrusted(lhs);
+ Assert(!trhs.isNull());
+ Trace("non-clausal-simplify")
+ << "substitute: will notify SAT layer of substitution: "
+ << trhs.getProven() << std::endl;
+ assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
+ trhs.getGenerator());
+ }
}
}
}
propagator->setNeedsFinish(true);
+
+ // Note that typically ttls.apply(assert)==assert here.
+ // However, this invariant is invalidated for cases where we use explicit
+ // equality assertions for variables solved in incremental mode that already
+ // exist in assertions, as described above.
+
return PreprocessingPassResult::NO_CONFLICT;
}
}
}
-void PreprocessingPassContext::addModelSubstitution(const Node& lhs,
- const Node& rhs)
-{
- getTheoryEngine()->getModel()->addSubstitution(lhs,
- d_smt->expandDefinitions(rhs));
-}
-
void PreprocessingPassContext::addSubstitution(const Node& lhs,
const Node& rhs,
ProofGenerator* pg)
{
getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg);
- // also add as a model substitution
- addModelSubstitution(lhs, rhs);
}
void PreprocessingPassContext::addSubstitution(const Node& lhs,
const std::vector<Node>& args)
{
getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args);
- // also add as a model substitution
- addModelSubstitution(lhs, rhs);
}
ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
void recordSymbolsInAssertions(const std::vector<Node>& assertions);
/**
- * Add substitution to theory model. This method should only be called if
- * we have already added the substitution to the top-level substitutions
- * class. Otherwise, addSubstitution should be called instead.
- * @param lhs The node replaced by node 'rhs'
- * @param rhs The node to substitute node 'lhs'
- */
- void addModelSubstitution(const Node& lhs, const Node& rhs);
- /**
- * Add substitution to the top-level substitutions and to the theory model.
+ * Add substitution to the top-level substitutions, which also as a
+ * consequence is used by the theory model.
* @param lhs The node replaced by node 'rhs'
* @param rhs The node to substitute node 'lhs'
* @param pg The proof generator that can provide a proof of lhs == rhs.
Debug("arith::ite") << "adding " << f << " -> " << t << endl;
d_subcount = d_subcount + 1;
d_subs->addSubstitution(f, t);
- d_model->addSubstitution(f, t);
}
Node ArithIteUtils::applySubstitutions(TNode f){
CombinationCareGraph::CombinationCareGraph(
TheoryEngine& te,
+ Env& env,
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm)
- : CombinationEngine(te, paraTheories, pnm)
+ : CombinationEngine(te, env, paraTheories, pnm)
{
}
{
public:
CombinationCareGraph(TheoryEngine& te,
+ Env& env,
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm);
~CombinationCareGraph();
namespace theory {
CombinationEngine::CombinationEngine(TheoryEngine& te,
+ Env& env,
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm)
: d_te(te),
+ d_env(env),
d_valuation(&te),
d_pnm(pnm),
d_logicInfo(te.getLogicInfo()),
d_eemanager.reset(
new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
// make the distributed model manager
- d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get()));
+ d_mmanager.reset(
+ new ModelManagerDistributed(d_te, d_env, *d_eemanager.get()));
}
else
{
namespace cvc5 {
class TheoryEngine;
+class Env;
namespace theory {
{
public:
CombinationEngine(TheoryEngine& te,
+ Env& env,
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm);
virtual ~CombinationEngine();
void sendLemma(TrustNode trn, TheoryId atomsTo);
/** Reference to the theory engine */
TheoryEngine& d_te;
+ /** Reference to the environment */
+ Env& d_env;
/** Valuation for the engine */
Valuation d_valuation;
/** The proof node manager */
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "prop/prop_engine.h"
-#include "theory/quantifiers_engine.h"
+#include "smt/env.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
namespace cvc5 {
namespace theory {
-ModelManager::ModelManager(TheoryEngine& te, EqEngineManager& eem)
+ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem)
: d_te(te),
- d_logicInfo(te.getLogicInfo()),
+ d_env(env),
d_eem(eem),
d_modelEqualityEngine(nullptr),
d_modelEqualityEngineAlloc(nullptr),
- d_model(new TheoryModel(te.getUserContext(),
- "DefaultModel",
- options::assignFunctionValues())),
+ d_model(new TheoryModel(
+ env, "DefaultModel", options::assignFunctionValues())),
d_modelBuilder(nullptr),
d_modelBuilt(false),
d_modelBuiltSuccess(false)
void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
{
// construct the model
- const LogicInfo& logicInfo = d_te.getLogicInfo();
+ const LogicInfo& logicInfo = d_env.getLogicInfo();
// Initialize the model and model builder.
if (logicInfo.isQuantified())
{
namespace cvc5 {
class TheoryEngine;
+class Env;
namespace theory {
class ModelManager
{
public:
- ModelManager(TheoryEngine& te, EqEngineManager& eem);
+ ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem);
virtual ~ModelManager();
/**
* Finish initializing this class, which allocates the model, the model
void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const;
/** Reference to the theory engine */
TheoryEngine& d_te;
- /** Logic info of theory engine (cached) */
- const LogicInfo& d_logicInfo;
+ /** Reference to the environment */
+ Env& d_env;
/** The equality engine manager */
EqEngineManager& d_eem;
/**
#include "theory/model_manager_distributed.h"
+#include "smt/env.h"
#include "theory/theory_engine.h"
#include "theory/theory_model.h"
#include "theory/theory_model_builder.h"
namespace theory {
ModelManagerDistributed::ModelManagerDistributed(TheoryEngine& te,
+ Env& env,
EqEngineManager& eem)
- : ModelManager(te, eem)
+ : ModelManager(te, env, eem)
{
}
// model, which includes both dump their equality information and assigning
// values. Notice the order of theories here is important and is the same
// as the list in CVC5_FOR_EACH_THEORY in theory_engine.cpp.
+ const LogicInfo& logicInfo = d_env.getLogicInfo();
for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
++theoryId)
{
- if (!d_logicInfo.isTheoryEnabled(theoryId))
+ if (!logicInfo.isTheoryEnabled(theoryId))
{
// theory not active, skip
continue;
#include "theory/model_manager.h"
namespace cvc5 {
-
-class TheoryEngine;
-
namespace theory {
/**
class ModelManagerDistributed : public ModelManager
{
public:
- ModelManagerDistributed(TheoryEngine& te, EqEngineManager& eem);
+ ModelManagerDistributed(TheoryEngine& te, Env& env, EqEngineManager& eem);
~ModelManagerDistributed();
/** Prepare the model, as described above. */
// Initialize the theory combination architecture
if (options::tcMode() == options::TcMode::CARE_GRAPH)
{
- d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm));
+ d_tc.reset(new CombinationCareGraph(*this, d_env, paraTheories, d_pnm));
}
else
{
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "options/uf_options.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
#include "theory/rewriter.h"
+#include "theory/trust_substitutions.h"
using namespace std;
using namespace cvc5::kind;
namespace cvc5 {
namespace theory {
-TheoryModel::TheoryModel(context::Context* c,
- std::string name,
- bool enableFuncModels)
- : d_name(name),
- d_substitutions(c),
+TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels)
+ : d_env(env),
+ d_name(name),
d_equalityEngine(nullptr),
d_using_model_core(false),
d_enableFuncModels(enableFuncModels)
Node TheoryModel::getValue(TNode n) const
{
//apply substitutions
- Node nn = d_substitutions.apply(n);
+ Node nn = d_env.getTopLevelSubstitutions().apply(n);
Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl;
//get value in model
nn = getModelValue(nn);
return n;
}
-/** add substitution */
-void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
- if( !d_substitutions.hasSubstitution( x ) ){
- Debug("model") << "Add substitution in model " << x << " -> " << t << std::endl;
- d_substitutions.addSubstitution( x, t, invalidateCache );
- } else {
-#ifdef CVC5_ASSERTIONS
- Node oldX = d_substitutions.getSubstitution(x);
- // check that either the old substitution is the same, or it now maps to the new substitution
- if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) {
- InternalError()
- << "Two incompatible substitutions added to TheoryModel:\n"
- << "the term: " << x << "\n"
- << "old mapping: " << d_substitutions.apply(oldX) << "\n"
- << "new mapping: " << d_substitutions.apply(t);
- }
-#endif /* CVC5_ASSERTIONS */
- }
-}
-
/** add term */
void TheoryModel::addTermInternal(TNode n)
{
Node n = it->first;
Assert(!n.isNull());
// should not have been solved for in a substitution
- Assert(d_substitutions.apply(n) == n);
+ Assert(d_env.getTopLevelSubstitutions().apply(n) == n);
if( !hasAssignedFunctionDefinition( n ) ){
Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl;
if( options::ufHo() ){
#include "theory/ee_setup_info.h"
#include "theory/rep_set.h"
-#include "theory/substitutions.h"
#include "theory/type_enumerator.h"
#include "theory/type_set.h"
#include "theory/uf/equality_engine.h"
namespace cvc5 {
+
+class Env;
+
namespace theory {
/** Theory Model class.
* (1) d_equalityEngine : an equality engine object, which stores
* an equivalence relation over all terms that exist in
* the current set of assertions.
- * (2) d_substitutions : a substitution map storing cases of
- * explicitly solved terms, for instance during preprocessing.
- * (3) d_reps : a map from equivalence class representatives of
+ * (2) d_reps : a map from equivalence class representatives of
* the equality engine to the (constant) representatives
* assigned to that equivalence class.
- * (4) d_uf_models : a map from uninterpreted functions to their
+ * (3) d_uf_models : a map from uninterpreted functions to their
* lambda representation.
- * (5) d_rep_set : a data structure that allows interpretations
+ * (4) d_rep_set : a data structure that allows interpretations
* for types to be represented as terms. This is useful for
* finite model finding.
+ * Additionally, models are dependent on top-level substitutions stored in the
+ * d_env class.
*
* These data structures are built after a full effort check with
* no lemmas sent, within a call to:
class TheoryModel
{
friend class TheoryEngineModelBuilder;
-public:
- TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
+
+ public:
+ TheoryModel(Env& env, std::string name, bool enableFuncModels);
virtual ~TheoryModel();
/**
* Finish init, where ee is the equality engine the model should use.
/** reset the model */
virtual void reset();
//---------------------------- for building the model
- /** Adds a substitution from x to t. */
- void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
/** assert equality holds in the model
*
* This method returns true if and only if the equality engine of this model
std::string debugPrintModelEqc() const;
protected:
+ /** Reference to the environmanet */
+ Env& d_env;
/** Unique name of this model */
std::string d_name;
- /** substitution map for this model */
- SubstitutionMap d_substitutions;
/** equality engine containing all known equalities/disequalities */
eq::EqualityEngine* d_equalityEngine;
/** approximations (see recordApproximation) */
-; COMMAND-LINE: -i --strings-exp
+; COMMAND-LINE: -i --strings-exp --no-check-models
; EXPECT: sat
(set-logic ALL)
(declare-fun str7 () String)
(assert (not (= str8 (str.replace_re_all (str.++ str9 str8 str7) (str.to_re "ULfQhzdcQSfqWSXyjuptqjqsazpyjzdDddlJPLDJhalmhBhlNBKZvoxoLOpfplkqhvIRHMOMDAGIdoRyiZmxmMvRijgpFnd") str9))))
(push)
(assert (and (str.in_re str8 (str.to_re str7)) (not (= str9 (str.replace_re_all (str.++ str8 str8) (str.to_re "ULfQhzdcQSfqWSXyjuptqjqsazpyjzdDddlJPLDJhalmhBhlNBKZvoxoLOpfplkqhvIRHMOMDAGIdoRyiZmxmMvRijgpFnd") str9)))))
+; note that (debug) model checking fails since this benchmark triggers a string variable (str7) to be solved after it appears in assertions, due to the push above.
+; this leads to a quantified formula changing after substitution, in which case our model evaluation loses track of its value.
(check-sat)
projects / cvc5.git / commitdiff