/*! \file theory_engine.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
+ ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY_ENGINE_H
-#define __CVC4__THEORY_ENGINE_H
+#ifndef CVC4__THEORY_ENGINE_H
+#define CVC4__THEORY_ENGINE_H
-#include <deque>
-#include <set>
+#include <memory>
#include <vector>
-#include <utility>
-#include "base/cvc4_assert.h"
-#include "context/cdhashset.h"
+#include "base/check.h"
+#include "context/cdhashmap.h"
#include "expr/node.h"
-#include "options/options.h"
-#include "options/smt_options.h"
-#include "prop/prop_engine.h"
-#include "smt/command.h"
-#include "smt_util/lemma_channels.h"
+#include "options/theory_options.h"
#include "theory/atom_requests.h"
-#include "theory/bv/bv_to_bool.h"
+#include "theory/engine_output_channel.h"
#include "theory/interrupted.h"
#include "theory/rewriter.h"
-#include "theory/shared_terms_database.h"
#include "theory/sort_inference.h"
-#include "theory/substitutions.h"
-#include "theory/term_registration_visitor.h"
#include "theory/theory.h"
+#include "theory/theory_preprocessor.h"
+#include "theory/trust_node.h"
+#include "theory/trust_substitutions.h"
#include "theory/uf/equality_engine.h"
#include "theory/valuation.h"
+#include "util/hash.h"
#include "util/statistics_registry.h"
#include "util/unsafe_interrupt_exception.h"
namespace CVC4 {
class ResourceManager;
-class LemmaProofRecipe;
+class OutputManager;
+class TheoryEngineProofGenerator;
/**
* A pair of a theory and a node. This is used to mark the flow of
* propagations between theories.
*/
struct NodeTheoryPair {
- Node node;
- theory::TheoryId theory;
- size_t timestamp;
- NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp = 0)
- : node(node), theory(theory), timestamp(timestamp) {}
- NodeTheoryPair()
- : theory(theory::THEORY_LAST) {}
+ Node d_node;
+ theory::TheoryId d_theory;
+ size_t d_timestamp;
+ NodeTheoryPair(TNode n, theory::TheoryId t, size_t ts = 0)
+ : d_node(n), d_theory(t), d_timestamp(ts)
+ {
+ }
+ NodeTheoryPair() : d_theory(theory::THEORY_LAST), d_timestamp() {}
// Comparison doesn't take into account the timestamp
bool operator == (const NodeTheoryPair& pair) const {
- return node == pair.node && theory == pair.theory;
+ return d_node == pair.d_node && d_theory == pair.d_theory;
}
};/* struct NodeTheoryPair */
NodeHashFunction hashFunction;
// Hash doesn't take into account the timestamp
size_t operator()(const NodeTheoryPair& pair) const {
- return hashFunction(pair.node)*0x9e3779b9 + pair.theory;
+ uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node));
+ return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash));
}
};/* struct NodeTheoryPairHashFunction */
/* Forward declarations */
namespace theory {
- class TheoryModel;
- class TheoryEngineModelBuilder;
- class ITEUtilities;
-
- namespace eq {
- class EqualityEngine;
- }/* CVC4::theory::eq namespace */
-
- namespace quantifiers {
- class TermDb;
- }
+class TheoryModel;
+class CombinationEngine;
+class SharedSolver;
+class DecisionManager;
+class RelevanceManager;
- class EntailmentCheckParameters;
- class EntailmentCheckSideEffects;
}/* CVC4::theory namespace */
-class DecisionEngine;
-class RemoveITE;
-class UnconstrainedSimplifier;
+namespace prop {
+class PropEngine;
+}
/**
* This is essentially an abstraction for a collection of theories. A
/** Shared terms database can use the internals notify the theories */
friend class SharedTermsDatabase;
- friend class theory::quantifiers::TermDb;
+ friend class theory::EngineOutputChannel;
+ friend class theory::CombinationEngine;
+ friend class theory::SharedSolver;
/** Associated PropEngine engine */
prop::PropEngine* d_propEngine;
- /** Access to decision engine */
- DecisionEngine* d_decisionEngine;
-
/** Our context */
context::Context* d_context;
* the cost of walking the DAG on registration, etc.
*/
const LogicInfo& d_logicInfo;
+ /** The separation logic location and data types */
+ TypeNode d_sepLocType;
+ TypeNode d_sepDataType;
- /**
- * The database of shared terms.
- */
- SharedTermsDatabase d_sharedTerms;
-
- /**
- * Master equality engine, to share with theories.
- */
- theory::eq::EqualityEngine* d_masterEqualityEngine;
-
- /** notify class for master equality engine */
- class NotifyClass : public theory::eq::EqualityEngineNotify {
- TheoryEngine& d_te;
- public:
- NotifyClass(TheoryEngine& te): d_te(te) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
- bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) {}
- void eqNotifyNewClass(TNode t) { d_te.eqNotifyNewClass(t); }
- void eqNotifyPreMerge(TNode t1, TNode t2) { d_te.eqNotifyPreMerge(t1, t2); }
- void eqNotifyPostMerge(TNode t1, TNode t2) { d_te.eqNotifyPostMerge(t1, t2); }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_te.eqNotifyDisequal(t1, t2, reason); }
- };/* class TheoryEngine::NotifyClass */
- NotifyClass d_masterEENotify;
+ /** Reference to the output manager of the smt engine */
+ OutputManager& d_outMgr;
- /**
- * notification methods
- */
- void eqNotifyNewClass(TNode t);
- void eqNotifyPreMerge(TNode t1, TNode t2);
- void eqNotifyPostMerge(TNode t1, TNode t2);
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
-
- /**
- * The quantifiers engine
- */
+ //--------------------------------- new proofs
+ /** Proof node manager used by this theory engine, if proofs are enabled */
+ ProofNodeManager* d_pnm;
+ /** The lazy proof object
+ *
+ * This stores instructions for how to construct proofs for all theory lemmas.
+ */
+ std::shared_ptr<LazyCDProof> d_lazyProof;
+ /** The proof generator */
+ std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
+ //--------------------------------- end new proofs
+ /** The combination manager we are using */
+ std::unique_ptr<theory::CombinationEngine> d_tc;
+ /** The shared solver of the above combination engine. */
+ theory::SharedSolver* d_sharedSolver;
+ /** The quantifiers engine, which is owned by the quantifiers theory */
theory::QuantifiersEngine* d_quantEngine;
-
- /**
- * Default model object
- */
- theory::TheoryModel* d_curr_model;
- bool d_aloc_curr_model;
- /**
- * Model builder object
- */
- theory::TheoryEngineModelBuilder* d_curr_model_builder;
-
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
- typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
-
- /**
- * Cache for theory-preprocessing of assertions
- */
- NodeMap d_ppCache;
-
- /**
- * Used for "missed-t-propagations" dumping mode only. A set of all
- * theory-propagable literals.
- */
- context::CDList<TNode> d_possiblePropagations;
-
- /**
- * Used for "missed-t-propagations" dumping mode only. A
- * context-dependent set of those theory-propagable literals that
- * have been propagated.
- */
- context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
-
-
- /**
- * Statistics for a particular theory.
- */
- class Statistics {
-
- static std::string mkName(std::string prefix,
- theory::TheoryId theory,
- std::string suffix) {
- std::stringstream ss;
- ss << prefix << theory << suffix;
- return ss.str();
- }
-
- public:
-
- IntStat conflicts, propagations, lemmas, requirePhase, flipDecision, restartDemands;
-
- Statistics(theory::TheoryId theory);
- ~Statistics();
- };/* class TheoryEngine::Statistics */
-
-
/**
- * An output channel for Theory that passes messages
- * back to a TheoryEngine.
+ * The decision manager
*/
- class EngineOutputChannel : public theory::OutputChannel {
+ std::unique_ptr<theory::DecisionManager> d_decManager;
+ /** The relevance manager */
+ std::unique_ptr<theory::RelevanceManager> d_relManager;
- friend class TheoryEngine;
-
- /**
- * The theory engine we're communicating with.
- */
- TheoryEngine* d_engine;
-
- /**
- * The statistics of the theory interractions.
- */
- Statistics d_statistics;
-
- /**
- * The theory owning this chanell.
- */
- theory::TheoryId d_theory;
-
- public:
-
- EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) :
- d_engine(engine),
- d_statistics(theory),
- d_theory(theory)
- {
- }
-
- void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
- spendResource(ammount);
- if (d_engine->d_interrupted) {
- throw theory::Interrupted();
- }
- }
-
- void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException);
-
- bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException);
-
- theory::LemmaStatus lemma(TNode lemma,
- ProofRule rule,
- bool removable = false,
- bool preprocess = false,
- bool sendAtoms = false);
-
- theory::LemmaStatus splitLemma(TNode lemma, bool removable = false);
-
- void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
- NodeManager* curr = NodeManager::currentNM();
- Node restartVar = curr->mkSkolem("restartVar",
- curr->booleanType(),
- "A boolean variable asserted to be true to force a restart");
- Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl;
- ++ d_statistics.restartDemands;
- lemma(restartVar, RULE_INVALID, true);
- }
-
- void requirePhase(TNode n, bool phase)
- throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
- Debug("theory") << "EngineOutputChannel::requirePhase("
- << n << ", " << phase << ")" << std::endl;
- ++ d_statistics.requirePhase;
- d_engine->d_propEngine->requirePhase(n, phase);
- }
-
- bool flipDecision()
- throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
- Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl;
- ++ d_statistics.flipDecision;
- return d_engine->d_propEngine->flipDecision();
- }
-
- void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
- Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
- d_engine->setIncomplete(d_theory);
- }
-
- void spendResource(unsigned ammount) throw(UnsafeInterruptException) {
- d_engine->spendResource(ammount);
- }
-
- void handleUserAttribute( const char* attr, theory::Theory* t ){
- d_engine->handleUserAttribute( attr, t );
- }
-
- private:
-
- /**
- * A helper function for registering lemma recipes with the proof engine
- */
- void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId);
- };/* class TheoryEngine::EngineOutputChannel */
+ /** are we in eager model building mode? (see setEagerModelBuilding). */
+ bool d_eager_model_building;
/**
* Output channels for individual theories.
*/
- EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
+ theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
/**
* Are we in conflict.
*/
context::CDO<bool> d_inConflict;
+ /**
+ * Are we in "SAT mode"? In this state, the user can query for the model.
+ * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB
+ * standard, version 2.6.
+ */
+ bool d_inSatMode;
+
/**
* Called by the theories to notify of a conflict.
+ *
+ * @param conflict The trust node containing the conflict and its proof
+ * generator (if it exists),
+ * @param theoryId The theory that sent the conflict
*/
- void conflict(TNode conflict, theory::TheoryId theoryId);
+ void conflict(theory::TrustNode conflict, theory::TheoryId theoryId);
/**
* Debugging flag to ensure that shutdown() is called before the
d_incomplete = true;
}
-
/**
* Mapping of propagations from recievers to senders.
*/
*/
void propagate(theory::Theory::Effort effort);
- /**
- * Called by the output channel to request decisions "as soon as
- * possible."
- */
- void propagateAsDecision(TNode literal, theory::TheoryId theory);
-
/**
* A variable to mark if we added any lemmas.
*/
/**
* Adds a new lemma, returning its status.
* @param node the lemma
- * @param negated should the lemma be asserted negated
- * @param removable can the lemma be remove (restrictions apply)
- * @param needAtoms if not THEORY_LAST, then
+ * @param p the properties of the lemma.
+ * @param atomsTo the theory that atoms of the lemma should be sent to
+ * @param from the theory that sent the lemma
*/
- theory::LemmaStatus lemma(TNode node,
- ProofRule rule,
- bool negated,
- bool removable,
- bool preprocess,
- theory::TheoryId atomsTo);
+ void lemma(theory::TrustNode node,
+ theory::LemmaProperty p,
+ theory::TheoryId atomsTo = theory::THEORY_LAST,
+ theory::TheoryId from = theory::THEORY_LAST);
/** Enusre that the given atoms are send to the given theory */
void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
- RemoveITE& d_iteRemover;
-
/** sort inference module */
SortInference d_sortInfer;
bool d_interrupted;
ResourceManager* d_resourceManager;
- /** Container for lemma input and output channels. */
- LemmaChannels* d_channels;
-
-public:
-
+ public:
/** Constructs a theory engine */
- TheoryEngine(context::Context* context, context::UserContext* userContext,
- RemoveITE& iteRemover, const LogicInfo& logic,
- LemmaChannels* channels);
+ TheoryEngine(context::Context* context,
+ context::UserContext* userContext,
+ ResourceManager* rm,
+ const LogicInfo& logic,
+ OutputManager& outMgr,
+ ProofNodeManager* pnm);
/** Destroys a theory engine */
~TheoryEngine();
- void interrupt() throw(ModalException);
- /**
- * "Spend" a resource during a search or preprocessing.
- */
- void spendResource(unsigned ammount);
+ void interrupt();
+
+ /** "Spend" a resource during a search or preprocessing.*/
+ void spendResource(ResourceManager::Resource r);
/**
* Adds a theory. Only one theory per TheoryId can be present, so if
* there is another theory it will be deleted.
*/
template <class TheoryClass>
- inline void addTheory(theory::TheoryId theoryId) {
+ inline void addTheory(theory::TheoryId theoryId)
+ {
Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
- d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
- d_theoryTable[theoryId] =
- new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId],
- theory::Valuation(this), d_logicInfo);
+ d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
+ d_theoryTable[theoryId] = new TheoryClass(d_context,
+ d_userContext,
+ *d_theoryOut[theoryId],
+ theory::Valuation(this),
+ d_logicInfo,
+ d_pnm);
+ theory::Rewriter::registerTheoryRewriter(
+ theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
}
- inline void setPropEngine(prop::PropEngine* propEngine) {
- Assert(d_propEngine == NULL);
+ void setPropEngine(prop::PropEngine* propEngine)
+ {
d_propEngine = propEngine;
}
- inline void setDecisionEngine(DecisionEngine* decisionEngine) {
- Assert(d_decisionEngine == NULL);
- d_decisionEngine = decisionEngine;
- }
-
- /** Called when all initialization of options/logic is done */
+ /**
+ * Called when all initialization of options/logic is done, after theory
+ * objects have been created.
+ *
+ * This initializes the quantifiers engine, the "official" equality engines
+ * of each theory as required, and the model and model builder utilities.
+ */
void finishInit();
/**
return d_propEngine;
}
+ /** Get the proof node manager */
+ ProofNodeManager* getProofNodeManager() const;
+
/**
* Get a pointer to the underlying sat context.
*/
- inline context::Context* getSatContext() const {
- return d_context;
- }
+ context::Context* getSatContext() const { return d_context; }
/**
* Get a pointer to the underlying user context.
*/
- inline context::Context* getUserContext() const {
- return d_userContext;
- }
+ context::UserContext* getUserContext() const { return d_userContext; }
/**
* Get a pointer to the underlying quantifiers engine.
theory::QuantifiersEngine* getQuantifiersEngine() const {
return d_quantEngine;
}
-
-private:
-
/**
- * Helper for preprocess
+ * Get a pointer to the underlying decision manager.
*/
- Node ppTheoryRewrite(TNode term);
+ theory::DecisionManager* getDecisionManager() const
+ {
+ return d_decManager.get();
+ }
+ private:
/**
* Queue of nodes for pre-registration.
*/
*/
context::CDO<bool> d_factsAsserted;
- /**
- * Map from equality atoms to theories that would like to be notified about them.
- */
-
-
/**
* Assert the formula to the given theory.
* @param assertion the assertion to send (not necesserily normalized)
* @param assertion the normalized assertion being sent
* @param originalAssertion the actual assertion that was sent
* @param toTheoryId the theory that is on the receiving end
- * @param fromTheoryId the theory that sent the assertino
+ * @param fromTheoryId the theory that sent the assertion
* @return true if a new assertion, false if theory already got it
*/
bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
/**
- * Computes the explanation by travarsing the propagation graph and
+ * Computes the explanation by traversing the propagation graph and
* asking relevant theories to explain the propagations. Initially
* the explanation vector should contain only the element (node, theory)
* where the node is the one to be explained, and the theory is the
- * theory that sent the literal. The lemmaProofRecipe will contain a list
- * of the explanation steps required to produce the original node.
+ * theory that sent the literal.
*/
- void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
+ theory::TrustNode getExplanation(
+ std::vector<NodeTheoryPair>& explanationVector);
-public:
+ /** Are proofs enabled? */
+ bool isProofEnabled() const;
+ public:
/**
- * Signal the start of a new round of assertion preprocessing
+ * Preprocess rewrite equality, called by the preprocessor to rewrite
+ * equalities appearing in the input.
*/
- void preprocessStart();
-
- /**
- * Runs theory specific preprocessing on the non-Boolean parts of
- * the formula. This is only called on input assertions, after ITEs
- * have been removed.
- */
- Node preprocess(TNode node);
+ theory::TrustNode ppRewriteEquality(TNode eq);
+ /** Notify (preprocessed) assertions. */
+ void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
-
- /**
- * Notify (preprocessed) assertions
- */
- void notifyPreprocessedAssertions( std::vector< Node >& assertions );
-
- /**
- * Return whether or not we are incomplete (in the current context).
- */
- inline bool isIncomplete() const {
- return d_incomplete;
- }
+ /** Return whether or not we are incomplete (in the current context). */
+ inline bool isIncomplete() const { return d_incomplete; }
/**
* Returns true if we need another round of checking. If this
inline bool needCheck() const {
return d_outputChannelUsed || d_lemmasAdded;
}
-
+ /**
+ * Is the literal lit (possibly) critical for satisfying the input formula in
+ * the current context? This call is applicable only during collectModelInfo
+ * or during LAST_CALL effort.
+ */
+ bool isRelevant(Node lit) const;
/**
* This is called at shutdown time by the SmtEngine, just before
* destruction. It is important because there are destruction
void shutdown();
/**
- * Solve the given literal with a theory that owns it.
+ * Solve the given literal with a theory that owns it. The proof of tliteral
+ * is carried in the trust node. The proof added to substitutionOut should
+ * take this proof into account (when proofs are enabled).
*/
- theory::Theory::PPAssertStatus solve(TNode literal,
- theory::SubstitutionMap& substitutionOut);
+ theory::Theory::PPAssertStatus solve(
+ theory::TrustNode tliteral,
+ theory::TrustSubstitutionMap& substitutionOut);
/**
* Preregister a Theory atom with the responsible theory (or
*/
void check(theory::Theory::Effort effort);
- /**
- * Run the combination framework.
- */
- void combineTheories();
-
/**
* Calls ppStaticLearn() on all theories, accumulating their
* combined contributions in the "learned" builder.
}
}
+ /**
+ * Returns the next decision request, or null if none exist. The next
+ * decision request is a literal that this theory engine prefers the SAT
+ * solver to make as its next decision. Decision requests are managed by
+ * the decision manager d_decManager.
+ */
Node getNextDecisionRequest();
bool properConflict(TNode conflict) const;
- bool properPropagation(TNode lit) const;
- bool properExplanation(TNode node, TNode expl) const;
/**
* Returns an explanation of the node propagated to the SAT solver.
*/
- Node getExplanation(TNode node);
+ theory::TrustNode getExplanation(TNode node);
/**
- * Returns an explanation of the node propagated to the SAT solver and the theory
- * that propagated it.
+ * Get the pointer to the model object used by this theory engine.
*/
- Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
-
+ theory::TheoryModel* getModel();
/**
- * collect model info
+ * Get the current model for the current set of assertions. This method
+ * should only be called immediately after a satisfiable or unknown
+ * response to a check-sat call, and only if produceModels is true.
+ *
+ * If the model is not already built, this will cause this theory engine
+ * to build the model.
+ *
+ * If the model is not available (for instance, if the last call to check-sat
+ * was interrupted), then this returns the null pointer.
*/
- void collectModelInfo( theory::TheoryModel* m, bool fullModel );
- /** post process model */
- void postProcessModel( theory::TheoryModel* m );
-
+ theory::TheoryModel* getBuiltModel();
/**
- * Get the current model
+ * This forces the model maintained by the combination engine to be built
+ * if it has not been done so already. This should be called only during a
+ * last call effort check after theory combination is run.
+ *
+ * @return true if the model was successfully built (possibly prior to this
+ * call).
*/
- theory::TheoryModel* getModel();
-
- /**
- * Get the model builder
+ bool buildModel();
+ /** set eager model building
+ *
+ * If this method is called, then this TheoryEngine will henceforth build
+ * its model immediately after every satisfiability check that results
+ * in a satisfiable or unknown result. The motivation for this mode is to
+ * accomodate API users that get the model object from the TheoryEngine,
+ * where we want to ensure that this model is always valid.
+ * TODO (#2648): revisit this.
*/
- theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; }
+ void setEagerModelBuilding() { d_eager_model_building = true; }
/**
* Get the theory associated to a given Node.
* @returns the theory
*/
inline theory::Theory* theoryOf(theory::TheoryId theoryId) const {
+ Assert(theoryId < theory::THEORY_LAST);
return d_theoryTable[theoryId];
}
inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
return d_logicInfo.isTheoryEnabled(theoryId);
}
+ /** get the logic info used by this theory engine */
+ const LogicInfo& getLogicInfo() const;
+ /** get the separation logic heap types */
+ bool getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const;
+
+ /**
+ * Declare heap. This is used for separation logics to set the location
+ * and data types. It should be called only once, and before any separation
+ * logic constraints are asserted to this theory engine.
+ */
+ void declareSepHeap(TypeNode locT, TypeNode dataT);
/**
* Returns the equality status of the two terms, from the theory
*/
Node getModelValue(TNode var);
- /**
- * Takes a literal and returns an equivalent literal that is guaranteed to be a SAT literal
- */
- Node ensureLiteral(TNode n);
-
- /**
- * Print all instantiations made by the quantifiers module.
- */
- void printInstantiations( std::ostream& out );
-
- /**
- * Print solution for synthesis conjectures found by ce_guided_instantiation module
- */
- void printSynthSolution( std::ostream& out );
-
- /**
- * Get list of quantified formulas that were instantiated
- */
- void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
-
- /**
- * Get instantiation methods
- * first inputs forall x.q[x] and returns ( q[a], ..., q[z] )
- * second inputs forall x.q[x] and returns ( a, ..., z )
- * third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) , ... , forall x.qn[x] -> ( qn[a]...qn[z] )
- */
- void getInstantiations( Node q, std::vector< Node >& insts );
- void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
- void getInstantiations( std::map< Node, std::vector< Node > >& insts );
- void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
-
- /**
- * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q.
- * Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q
- */
- Node getInstantiatedConjunction( Node q );
-
/**
* Forwards an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
*/
- std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
-
-private:
+ std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
- /** Default visitor for pre-registration */
- PreRegisterVisitor d_preRegistrationVisitor;
-
- /** Visitor for collecting shared terms */
- SharedTermsVisitor d_sharedTermsVisitor;
+ private:
/** Dump the assertions to the dump */
void dumpAssertions(const char* tag);
- /**
- * A collection of ite preprocessing passes.
- */
- theory::ITEUtilities* d_iteUtilities;
-
-
- /** For preprocessing pass simplifying unconstrained expressions */
- UnconstrainedSimplifier* d_unconstrainedSimp;
-
/** For preprocessing pass lifting bit-vectors of size 1 to booleans */
- theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor;
public:
- void staticInitializeBVOptions(const std::vector<Node>& assertions);
- void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
- bool ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
- void mkAckermanizationAsssertions(std::vector<Node>& assertions);
-
- Node ppSimpITE(TNode assertion);
- /** Returns false if an assertion simplified to false. */
- bool donePPSimpITE(std::vector<Node>& assertions);
-
- void ppUnconstrainedSimp(std::vector<Node>& assertions);
-
- SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
-
- theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
-
- RemoveITE* getIteRemover() { return &d_iteRemover; }
SortInference* getSortInference() { return &d_sortInfer; }
/** Prints the assertions to the debug stream */
void printAssertions(const char* tag);
- /** Theory alternative is in use. */
- bool useTheoryAlternative(const std::string& name);
-
- /** Enables using a theory alternative by name. */
- void enableTheoryAlternative(const std::string& name);
-
private:
- std::set< std::string > d_theoryAlternatives;
std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
-public:
- /**
- * Set user attribute.
- * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done
- * via the syntax (! n :attr)
+ public:
+ /** Set user attribute.
+ *
+ * This function is called when an attribute is set by a user. In SMT-LIBv2
+ * this is done via the syntax (! n :attr)
*/
- void setUserAttribute(const std::string& attr, Node n, std::vector<Node>& node_values, std::string str_value);
+ void setUserAttribute(const std::string& attr,
+ Node n,
+ const std::vector<Node>& node_values,
+ const std::string& str_value);
- /**
- * Handle user attribute.
+ /** Handle user attribute.
+ *
* Associates theory t with the attribute attr. Theory t will be
* notified whenever an attribute of name attr is set.
*/
* Check that the theory assertions are satisfied in the model.
* This function is called from the smt engine's checkModel routine.
*/
- void checkTheoryAssertionsWithModel();
-
-private:
- IntStat d_arithSubstitutionsAdded;
-
+ void checkTheoryAssertionsWithModel(bool hardFailure);
};/* class TheoryEngine */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY_ENGINE_H */
+#endif /* CVC4__THEORY_ENGINE_H */
projects / cvc5.git / blobdiff