/*! \file theory.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 "context/cdo.h"
#include "context/context.h"
#include "expr/node.h"
-#include "lib/ffs.h"
#include "options/options.h"
#include "options/theory_options.h"
-#include "smt/command.h"
-#include "smt/dump.h"
#include "smt/logic_request.h"
#include "theory/assertion.h"
#include "theory/care_graph.h"
#include "theory/logic_info.h"
#include "theory/output_channel.h"
#include "theory/theory_id.h"
+#include "theory/theory_inference_manager.h"
#include "theory/theory_rewriter.h"
#include "theory/theory_state.h"
#include "theory/trust_node.h"
+#include "theory/trust_substitutions.h"
#include "theory/valuation.h"
#include "util/statistics_registry.h"
/** Information about the logic we're operating within. */
const LogicInfo& d_logicInfo;
- /** Pointer to proof node manager */
- ProofNodeManager* d_pnm;
-
/**
* The assertFact() queue.
*
/** Index into the head of the facts list */
context::CDO<unsigned> d_factsHead;
- /** Add shared term to the theory. */
- void addSharedTermInternal(TNode node);
-
/** Indices for splitting on the shared terms. */
context::CDO<unsigned> d_sharedTermsIndex;
/** The care graph the theory will use during combination. */
CareGraph* d_careGraph;
- /**
- * Pointer to the quantifiers engine (or NULL, if quantifiers are not
- * supported or not enabled). Not owned by the theory.
- */
- QuantifiersEngine* d_quantEngine;
-
/** Pointer to the decision manager. */
DecisionManager* d_decManager;
*/
context::CDList<TNode> d_sharedTerms;
- //---------------------------------- collect model info
- /**
- * Scans the current set of assertions and shared terms top-down
- * until a theory-leaf is reached, and adds all terms found to
- * termSet. This is used by collectModelInfo to delimit the set of
- * terms that should be used when constructing a model.
- *
- * irrKinds: The kinds of terms that appear in assertions that should *not*
- * be included in termSet. Note that the kinds EQUAL and NOT are always
- * treated as irrelevant kinds.
- *
- * includeShared: Whether to include shared terms in termSet. Notice that
- * shared terms are not influenced by irrKinds.
- */
- void computeRelevantTermsInternal(std::set<Node>& termSet,
- std::set<Kind>& irrKinds,
- bool includeShared = true) const;
- /**
- * Helper function for computeRelevantTerms
- */
- void collectTerms(TNode n,
- std::set<Kind>& irrKinds,
- std::set<Node>& termSet) const;
- /**
- * Same as above, but with empty irrKinds. This version can be overridden
- * by the theory, e.g. by restricting or extending the set of terms returned
- * by computeRelevantTermsInternal, which is called by default with no
- * irrKinds.
- */
- virtual void computeRelevantTerms(std::set<Node>& termSet,
- bool includeShared = true);
- /**
- * Collect model values, after equality information is added to the model.
- * The argument termSet is the set of relevant terms returned by
- * computeRelevantTerms.
- */
- virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet);
- //---------------------------------- end collect model info
-
/**
* Construct a Theory.
*
*/
TheoryState* d_theoryState;
/**
- * Whether proofs are enabled
+ * The theory inference manager. This is a wrapper around the equality
+ * engine and the output channel. It ensures that the output channel and
+ * the equality engine are used properly.
+ */
+ TheoryInferenceManager* d_inferManager;
+
+ /**
+ * Pointer to the quantifiers engine (or NULL, if quantifiers are not
+ * supported or not enabled). Not owned by the theory.
+ */
+ QuantifiersEngine* d_quantEngine;
+
+ /** Pointer to proof node manager */
+ ProofNodeManager* d_pnm;
+
+ /**
+ * Are proofs enabled?
*
+ * They are considered enabled if the ProofNodeManager is non-null.
*/
- bool d_proofsEnabled;
+ bool proofsEnabled() const;
/**
* Returns the next assertion in the assertFact() queue.
return d_logicInfo;
}
+ /**
+ * Set separation logic heap. This is called when the location and data
+ * types for separation logic are determined. This should be called at
+ * most once, before solving.
+ *
+ * This currently should be overridden by the separation logic theory only.
+ */
+ virtual void declareSepHeap(TypeNode locT, TypeNode dataT) {}
+
/**
* The theory that owns the uninterpreted sort.
*/
virtual void finishInit() {}
//--------------------------------- end private initialization
+ /**
+ * This method is called to notify a theory that the node n should
+ * be considered a "shared term" by this theory. This does anything
+ * theory-specific concerning the fact that n is now marked as a shared
+ * term, which is done in addition to explicitly storing n as a shared
+ * term and adding it as a trigger term in the equality engine of this
+ * class (see addSharedTerm).
+ */
+ virtual void notifySharedTerm(TNode n);
+
public:
//--------------------------------- initialization
/**
* Normally we call QUICK_CHECK or STANDARD; at the leaves we call
* with FULL_EFFORT.
*/
- enum Effort {
+ enum Effort
+ {
/**
* Standard effort where theory need not do anything
*/
EFFORT_STANDARD = 50,
/**
- * Full effort requires the theory make sure its assertions are satisfiable or not
+ * Full effort requires the theory make sure its assertions are satisfiable
+ * or not
*/
EFFORT_FULL = 100,
/**
- * Combination effort means that the individual theories are already satisfied, and
- * it is time to put some effort into propagation of shared term equalities
- */
- EFFORT_COMBINATION = 150,
- /**
- * Last call effort, reserved for quantifiers.
+ * Last call effort, called after theory combination has completed with
+ * no lemmas and a model is available.
*/
EFFORT_LAST_CALL = 200
- };/* enum Effort */
+ }; /* enum Effort */
static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
{ return e >= EFFORT_STANDARD; }
{ return e >= EFFORT_STANDARD && e < EFFORT_FULL; }
static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
{ return e == EFFORT_FULL; }
- static inline bool combination(Effort e) CVC4_CONST_FUNCTION
- { return e == EFFORT_COMBINATION; }
/**
* Get the id for this Theory.
return d_valuation;
}
+ /** Get the equality engine being used by this theory. */
+ eq::EqualityEngine* getEqualityEngine();
+
/**
* Get the quantifiers engine associated to this theory.
*/
return d_quantEngine;
}
+ /** Get the decision manager associated to this theory. */
+ DecisionManager* getDecisionManager() { return d_decManager; }
+
/**
- * Get the quantifiers engine associated to this theory (const version).
+ * @return The theory state associated with this theory.
*/
- const QuantifiersEngine* getQuantifiersEngine() const {
- return d_quantEngine;
- }
+ TheoryState* getTheoryState() { return d_theoryState; }
- /** Get the decision manager associated to this theory. */
- DecisionManager* getDecisionManager() { return d_decManager; }
+ /**
+ * @return The theory inference manager associated with this theory.
+ */
+ TheoryInferenceManager* getInferenceManager() { return d_inferManager; }
/**
* Expand definitions in the term node. This returns a term that is
/**
* Pre-register a term. Done one time for a Node per SAT context level.
*/
- virtual void preRegisterTerm(TNode) { }
+ virtual void preRegisterTerm(TNode);
/**
* Assert a fact in the current context.
d_facts.push_back(Assertion(assertion, isPreregistered));
}
- /**
- * This method is called to notify a theory that the node n should
- * be considered a "shared term" by this theory
- */
- virtual void addSharedTerm(TNode n) { }
-
- /**
- * Get the official equality engine of this theory.
- */
- eq::EqualityEngine* getEqualityEngine();
+ /** Add shared term to the theory. */
+ void addSharedTerm(TNode node);
/**
* Return the current theory care graph. Theories should overload
* Return the status of two terms in the current context. Should be
* implemented in sub-theories to enable more efficient theory-combination.
*/
- virtual EqualityStatus getEqualityStatus(TNode a, TNode b) {
- return EQUALITY_UNKNOWN;
- }
+ virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
/**
* Return the model value of the give shared term (or null if not available).
- */
- virtual Node getModelValue(TNode var) { return Node::null(); }
-
- /**
- * Check the current assignment's consistency.
*
- * An implementation of check() is required to either:
- * - return a conflict on the output channel,
- * - be interrupted,
- * - throw an exception
- * - or call get() until done() is true.
+ * TODO (project #39): this method is likely to become deprecated.
*/
- virtual void check(Effort level = EFFORT_FULL) { }
-
- /** Needs last effort check? */
- virtual bool needsCheckLastEffort() { return false; }
+ virtual Node getModelValue(TNode var) { return Node::null(); }
/** T-propagate new literal assignments in the current context. */
- virtual void propagate(Effort level = EFFORT_FULL) { }
+ virtual void propagate(Effort level = EFFORT_FULL) {}
/**
* Return an explanation for the literal represented by parameter n
Unimplemented() << "Theory " << identify()
<< " propagated a node but doesn't implement the "
"Theory::explain() interface!";
+ return TrustNode::null();
}
+ //--------------------------------- check
+ /**
+ * Does this theory wish to be called to check at last call effort? This is
+ * the case for any theory that wishes to run when a model is available.
+ */
+ virtual bool needsCheckLastEffort() { return false; }
+ /**
+ * Check the current assignment's consistency.
+ *
+ * An implementation of check() is required to either:
+ * - return a conflict on the output channel,
+ * - be interrupted,
+ * - throw an exception
+ * - or call get() until done() is true.
+ *
+ * The standard method for check consists of a loop that processes the entire
+ * fact queue when preCheck returns false. It makes four theory-specific
+ * callbacks, (preCheck, postCheck, preNotifyFact, notifyFact) as described
+ * below. It asserts each fact to the official equality engine when
+ * preNotifyFact returns false.
+ *
+ * Theories that use this check method must use an official theory
+ * state object (d_theoryState).
+ */
+ void check(Effort level = EFFORT_FULL);
+ /**
+ * Pre-check, called before the fact queue of the theory is processed.
+ * If this method returns false, then the theory will process its fact
+ * queue. If this method returns true, then the theory has indicated
+ * its check method should finish immediately.
+ */
+ virtual bool preCheck(Effort level = EFFORT_FULL);
+ /**
+ * Post-check, called after the fact queue of the theory is processed.
+ */
+ virtual void postCheck(Effort level = EFFORT_FULL);
+ /**
+ * Pre-notify fact, return true if the theory processed it. If this
+ * method returns false, then the atom will be added to the equality engine
+ * of the theory and notifyFact will be called with isInternal=false.
+ *
+ * Theories that implement check but do not use official equality
+ * engines should always return true for this method.
+ *
+ * @param atom The atom
+ * @param polarity Its polarity
+ * @param fact The original literal that was asserted
+ * @param isPrereg Whether the assertion is preregistered
+ * @param isInternal Whether the origin of the fact was internal. If this
+ * is false, the fact was asserted via the fact queue of the theory.
+ * @return true if the theory completely processed this fact, i.e. it does
+ * not need to assert the fact to its equality engine.
+ */
+ virtual bool preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal);
+ /**
+ * Notify fact, called immediately after the fact was pushed into the
+ * equality engine.
+ *
+ * @param atom The atom
+ * @param polarity Its polarity
+ * @param fact The original literal that was asserted.
+ * @param isInternal Whether the origin of the fact was internal. If this
+ * is false, the fact was asserted via the fact queue of the theory.
+ */
+ virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal);
+ //--------------------------------- end check
+
+ //--------------------------------- collect model info
/**
* Get all relevant information in this theory regarding the current
* model. This should be called after a call to check( FULL_EFFORT )
*
* This method returns true if and only if the equality engine of m is
* consistent as a result of this call.
+ *
+ * The standard method for collectModelInfo computes the relevant terms,
+ * asserts the theory's equality engine to the model (if necessary) and
+ * then calls computeModelValues.
+ *
+ * TODO (project #39): this method should be non-virtual, once all theories
+ * conform to the new standard, delete, move to model manager distributed.
+ */
+ virtual bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet);
+ /**
+ * Compute terms that are not necessarily part of the assertions or
+ * shared terms that should be considered relevant, add them to termSet.
+ */
+ virtual void computeRelevantTerms(std::set<Node>& termSet);
+ /**
+ * Collect model values, after equality information is added to the model.
+ * The argument termSet is the set of relevant terms returned by
+ * computeRelevantTerms.
*/
- virtual bool collectModelInfo(TheoryModel* m);
+ virtual bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet);
/** if theories want to do something with model after building, do it here */
virtual void postProcessModel( TheoryModel* m ){ }
+ //--------------------------------- end collect model info
+
+ //--------------------------------- preprocessing
/**
* Statically learn from assertion "in," which has been asserted
* true at the top level. The theory should only add (via
};
/**
- * Given a literal, add the solved substitutions to the map, if any.
- * The method should return true if the literal can be safely removed.
+ * Given a literal and its proof generator (encapsulated by trust node tin),
+ * add the solved substitutions to the map, if any. The method should return
+ * true if the literal can be safely removed from the input problem.
+ *
+ * Note that tin has trude node kind LEMMA. Its proof generator should be
+ * take into account when adding a substitution to outSubstitutions when
+ * proofs are enabled.
*/
- virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ virtual PPAssertStatus ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions);
/**
- * Given an atom of the theory coming from the input formula, this
- * method can be overridden in a theory implementation to rewrite
- * the atom into an equivalent form. This is only called just
- * before an input atom to the engine. This method returns a TrustNode of
- * kind TrustNodeKind::REWRITE, which carries information about the proof
- * generator for the rewrite. Similarly to expandDefinition, this method may
- * return the null TrustNode if atom is unchanged.
+ * Given a term of the theory coming from the input formula or
+ * from a lemma generated during solving, this method can be overridden in a
+ * theory implementation to rewrite the term into an equivalent form.
+ *
+ * This method returns a TrustNode of kind TrustNodeKind::REWRITE, which
+ * carries information about the proof generator for the rewrite, which can
+ * be the null TrustNode if n is unchanged.
+ *
+ * Notice this method is used both in the "theory rewrite equalities"
+ * preprocessing pass, where n is an equality from the input formula,
+ * and in theory preprocessing, where n is a (non-equality) term occurring
+ * in the input or generated in a lemma.
*/
- virtual TrustNode ppRewrite(TNode atom) { return TrustNode::null(); }
+ virtual TrustNode ppRewrite(TNode n) { return TrustNode::null(); }
/**
* Notify preprocessed assertions. Called on new assertions after
* preprocessing before they are asserted to theory engine.
*/
virtual void ppNotifyAssertions(const std::vector<Node>& assertions) {}
+ //--------------------------------- end preprocessing
/**
* A Theory is called with presolve exactly one time per user
<< " doesn't support Theory::setUserAttribute interface";
}
- /** A set of theories */
- typedef uint32_t Set;
-
- /** A set of all theories */
- static const Set AllTheories = (1 << theory::THEORY_LAST) - 1;
-
- /** Pops a first theory off the set */
- static inline TheoryId setPop(Set& set) {
- uint32_t i = ffs(set); // Find First Set (bit)
- if (i == 0) { return THEORY_LAST; }
- TheoryId id = (TheoryId)(i-1);
- set = setRemove(id, set);
- return id;
- }
-
- /** Returns the size of a set of theories */
- static inline size_t setSize(Set set) {
- size_t count = 0;
- while (setPop(set) != THEORY_LAST) {
- ++ count;
- }
- return count;
- }
-
- /** Returns the index size of a set of theories */
- static inline size_t setIndex(TheoryId id, Set set) {
- Assert(setContains(id, set));
- size_t count = 0;
- while (setPop(set) != id) {
- ++ count;
- }
- return count;
- }
-
- /** Add the theory to the set. If no set specified, just returns a singleton set */
- static inline Set setInsert(TheoryId theory, Set set = 0) {
- return set | (1 << theory);
- }
-
- /** Add the theory to the set. If no set specified, just returns a singleton set */
- static inline Set setRemove(TheoryId theory, Set set = 0) {
- return setDifference(set, setInsert(theory));
- }
-
- /** Check if the set contains the theory */
- static inline bool setContains(TheoryId theory, Set set) {
- return set & (1 << theory);
- }
-
- static inline Set setComplement(Set a) {
- return (~a) & AllTheories;
- }
-
- static inline Set setIntersection(Set a, Set b) {
- return a & b;
- }
-
- static inline Set setUnion(Set a, Set b) {
- return a | b;
- }
-
- /** a - b */
- static inline Set setDifference(Set a, Set b) {
- return (~b) & a;
- }
-
- static inline std::string setToString(theory::Theory::Set theorySet) {
- std::stringstream ss;
- ss << "[";
- for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
- if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) {
- ss << (theory::TheoryId) theoryId << " ";
- }
- }
- ss << "]";
- return ss.str();
- }
-
typedef context::CDList<Assertion>::const_iterator assertions_iterator;
/**
*
* @return true iff facts have been asserted to this theory.
*/
- bool hasFacts() {
- return !d_facts.empty();
- }
+ bool hasFacts() { return !d_facts.empty(); }
/** Return total number of facts asserted to this theory */
size_t numAssertions() {
return d_facts.size();
}
-
+
typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
/**
* E |= lit in the theory.
*/
virtual std::pair<bool, Node> entailmentCheck(TNode lit);
-
- /* get current substitution at an effort
- * input : vars
- * output : subs, exp
- * where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
- */
- virtual bool getCurrentSubstitution(int effort, std::vector<Node>& vars,
- std::vector<Node>& subs,
- std::map<Node, std::vector<Node> >& exp) {
- return false;
- }
-
- /* is extended function reduced */
- virtual bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ) { return n.isConst(); }
-
- /**
- * Get reduction for node
- * If return value is not 0, then n is reduced.
- * If return value <0 then n is reduced SAT-context-independently (e.g. by a
- * lemma that persists at this user-context level).
- * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
- * and return value should be <0.
- */
- virtual int getReduction( int effort, Node n, Node& nr ) { return 0; }
-
- /** Turn on proof-production mode. */
- void produceProofs() { d_proofsEnabled = true; }
-
};/* class Theory */
std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
- if(Dump.isOn("state")) {
- Dump("state") << AssertCommand(fact.d_assertion.toExpr());
- }
-
return fact;
}
projects / cvc5.git / blobdiff