#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.
*
/** 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;
- //---------------------------------- private collect model info
- /**
- * Helper function for computeRelevantTerms
- */
- void collectTerms(TNode n,
- const std::set<Kind>& irrKinds,
- std::set<Node>& termSet) const;
- //---------------------------------- end private collect model info
-
/**
* Construct a Theory.
*
*/
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 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.
*/
/** Get the decision manager associated to this theory. */
DecisionManager* getDecisionManager() { return d_decManager; }
+ /**
+ * @return The theory state associated with this theory.
+ */
+ TheoryState* getTheoryState() { return d_theoryState; }
+
+ /**
+ * @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
* equivalent to node. It wraps this term in a TrustNode of kind
*
* Theories that use this check method must use an official theory
* state object (d_theoryState).
- *
- * TODO (project #39): this method should be non-virtual, once all theories
- * conform to the new standard
*/
- virtual void check(Effort level = EFFORT_FULL);
+ 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
* then calls computeModelValues.
*
* TODO (project #39): this method should be non-virtual, once all theories
- * conform to the new standard
+ * conform to the new standard, delete, move to model manager distributed.
*/
- virtual bool collectModelInfo(TheoryModel* m);
- /**
- * 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.
- *
- * @param 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.
- *
- * @param includeShared Whether to include shared terms in termSet. Notice that
- * shared terms are not influenced by irrKinds.
- *
- * TODO (project #39): this method will be deleted. The version in
- * model manager will be used.
- */
- void computeAssertedTerms(std::set<Node>& termSet,
- const std::set<Kind>& irrKinds,
- bool includeShared = true) const;
+ 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.
};
/**
- * 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
projects / cvc5.git / blobdiff