/*! \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.
*
/** 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
- /**
- * 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;
- //---------------------------------- end private 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.
*/
/** 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
Unimplemented() << "Theory " << identify()
<< " propagated a node but doesn't implement the "
"Theory::explain() interface!";
+ return TrustNode::null();
}
//--------------------------------- check
*
* 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
* @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);
+ 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
+ * @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
* 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);
+ virtual bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet);
/**
- * 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.
+ * 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,
- bool includeShared = true);
+ 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 collectModelValues(TheoryModel* m, std::set<Node>& termSet);
+ 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
};
/**
- * 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
<< " 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