#include "options/theory_options.h"
#include "proof/trust_node.h"
#include "smt/env.h"
+#include "smt/env_obj.h"
#include "theory/assertion.h"
#include "theory/care_graph.h"
#include "theory/logic_info.h"
namespace eq {
class EqualityEngine;
- } // namespace eq
+} // namespace eq
/**
* Base class for T-solvers. Abstract DPLL(T).
* Initialization of the second form happens during TheoryEngine::finishInit,
* after the quantifiers engine and model objects have been set up.
*/
-class Theory {
+class Theory : protected EnvObj
+{
friend class ::cvc5::TheoryEngine;
private:
/** An integer identifying the type of the theory. */
TheoryId d_id;
- /** The environment class */
- Env& d_env;
-
/**
* The assertFact() queue.
*
DecisionManager* d_decManager;
protected:
- /** Name of this theory instance. Along with the TheoryId this should provide
- * an unique string identifier for each instance of a Theory class. We need
- * this to ensure unique statistics names over multiple theory instances. */
+ /** Name of this theory instance. Along with the TheoryId this should
+ * provide an unique string identifier for each instance of a Theory class.
+ * We need this to ensure unique statistics names over multiple theory
+ * instances. */
std::string d_instanceName;
// === STATISTICS ===
* you must make an explicit call here to this->Theory::shutdown()
* too.
*/
- virtual void shutdown() { }
+ virtual void shutdown() {}
/**
* The output channel for the Theory.
*/
std::unique_ptr<eq::EqualityEngine> d_allocEqualityEngine;
/**
- * The theory state, which contains contexts, valuation, and equality engine.
- * Notice the theory is responsible for memory management of this class.
+ * The theory state, which contains contexts, valuation, and equality
+ * engine. Notice the theory is responsible for memory management of this
+ * class.
*/
TheoryState* d_theoryState;
/**
*/
inline Assertion get();
- const LogicInfo& getLogicInfo() const { return d_env.getLogicInfo(); }
-
/**
* Set separation logic heap. This is called when the location and data
* types for separation logic are determined. This should be called at
* The following criteria imply that x -> val is *not* a legal elimination:
* (1) If x is contained in val,
* (2) If the type of val is not a subtype of the type of x,
- * (3) If val contains an operator that cannot be evaluated, and produceModels
- * is true. For example, x -> sqrt(2) is not a legal elimination if we
- * are producing models. This is because we care about the value of x, and
- * its value must be computed (approximated) by the non-linear solver.
+ * (3) If val contains an operator that cannot be evaluated, and
+ * produceModels is true. For example, x -> sqrt(2) is not a legal
+ * elimination if we are producing models. This is because we care about the
+ * value of x, and its value must be computed (approximated) by the
+ * non-linear solver.
*/
bool isLegalElimination(TNode x, TNode val);
//--------------------------------- private initialization
*/
virtual void notifySharedTerm(TNode n);
/**
- * Notify in conflict, called when a conflict clause is added to TheoryEngine
- * by any theory (not necessarily this one). This signals that the theory
- * should suspend what it is currently doing and wait for backtracking.
+ * Notify in conflict, called when a conflict clause is added to
+ * TheoryEngine by any theory (not necessarily this one). This signals that
+ * the theory should suspend what it is currently doing and wait for
+ * backtracking.
*/
virtual void notifyInConflict();
* initialize its equality engine field via setEqualityEngine above during
* TheoryEngine::finishInit, prior to calling finishInit for this theory.
*
- * Additionally, if this method returns true, then this method is required to
- * update the argument esi with instructions for initializing and setting up
- * notifications from its equality engine, which is commonly done with
- * a notifications class (eq::EqualityEngineNotify).
+ * Additionally, if this method returns true, then this method is required
+ * to update the argument esi with instructions for initializing and setting
+ * up notifications from its equality engine, which is commonly done with a
+ * notifications class (eq::EqualityEngineNotify).
*/
virtual bool needsEqualityEngine(EeSetupInfo& esi);
/**
/**
* Return the ID of the theory responsible for the given type.
*/
- static inline TheoryId theoryOf(TypeNode typeNode) {
+ static inline TheoryId theoryOf(TypeNode typeNode)
+ {
Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
TheoryId id;
- if (typeNode.getKind() == kind::TYPE_CONSTANT) {
+ if (typeNode.getKind() == kind::TYPE_CONSTANT)
+ {
id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
- } else {
+ }
+ else
+ {
id = kindToTheoryId(typeNode.getKind());
}
- if (id == THEORY_BUILTIN) {
- Trace("theory::internal") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
+ if (id == THEORY_BUILTIN)
+ {
+ Trace("theory::internal")
+ << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner
+ << std::endl;
return s_uninterpretedSortOwner;
}
return id;
/**
* Returns the ID of the theory responsible for the given node.
*/
- static inline TheoryId theoryOf(TNode node) {
+ static inline TheoryId theoryOf(TNode node)
+ {
return theoryOf(options::theoryOfMode(), node);
}
/**
* Set the owner of the uninterpreted sort.
*/
- static void setUninterpretedSortOwner(TheoryId theory) {
+ static void setUninterpretedSortOwner(TheoryId theory)
+ {
s_uninterpretedSortOwner = theory;
}
/**
* Get the owner of the uninterpreted sort.
*/
- static TheoryId getUninterpretedSortOwner() {
+ static TheoryId getUninterpretedSortOwner()
+ {
return s_uninterpretedSortOwner;
}
/**
* Checks if the node is a leaf node of this theory
*/
- inline bool isLeaf(TNode node) const {
+ inline bool isLeaf(TNode node) const
+ {
return node.getNumChildren() == 0 || theoryOf(node) != d_id;
}
/**
* Checks if the node is a leaf node of a theory.
*/
- inline static bool isLeafOf(TNode node, TheoryId theoryId) {
+ inline static bool isLeafOf(TNode node, TheoryId theoryId)
+ {
return node.getNumChildren() == 0 || theoryOf(node) != theoryId;
}
*/
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,
/**
static inline bool standardEffortOrMore(Effort e) CVC5_CONST_FUNCTION
{
- return e >= EFFORT_STANDARD; }
+ return e >= EFFORT_STANDARD;
+ }
static inline bool standardEffortOnly(Effort e) CVC5_CONST_FUNCTION
{
- return e >= EFFORT_STANDARD && e < EFFORT_FULL; }
+ return e >= EFFORT_STANDARD && e < EFFORT_FULL;
+ }
static inline bool fullEffort(Effort e) CVC5_CONST_FUNCTION
{
- return e == EFFORT_FULL; }
+ return e == EFFORT_FULL;
+ }
/**
* Get the id for this Theory.
*/
- TheoryId getId() const {
- return d_id;
- }
+ TheoryId getId() const { return d_id; }
/**
* Get a reference to the environment.
/**
* Get the context associated to this Theory.
*/
- context::UserContext* getUserContext() const {
+ context::UserContext* getUserContext() const
+ {
return d_env.getUserContext();
}
/**
* Get the output channel associated to this theory.
*/
- OutputChannel& getOutputChannel() {
- return *d_out;
- }
+ OutputChannel& getOutputChannel() { return *d_out; }
/**
* Get the valuation associated to this theory.
*/
- Valuation& getValuation() {
- return d_valuation;
- }
+ Valuation& getValuation() { return d_valuation; }
/** Get the equality engine being used by this theory. */
eq::EqualityEngine* getEqualityEngine();
/**
* Get the quantifiers engine associated to this theory.
*/
- QuantifiersEngine* getQuantifiersEngine() {
- return d_quantEngine;
- }
+ QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
/**
* @return The theory state associated with this theory.
/**
* Assert a fact in the current context.
*/
- void assertFact(TNode assertion, bool isPreregistered) {
+ void assertFact(TNode assertion, bool isPreregistered)
+ {
Trace("theory") << "Theory<" << getId() << ">::assertFact["
<< getSatContext()->getLevel() << "](" << assertion << ", "
<< (isPreregistered ? "true" : "false") << ")" << std::endl;
virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
/**
- * Return the model value of the give shared term (or null if not available).
+ * Return the model value of the give shared term (or null if not
+ * available).
*
* TODO (project #39): this method is likely to become deprecated.
*/
* - 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.
+ * 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).
*/
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 ){ }
+ /** if theories want to do something with model after building, do it here
+ */
+ virtual void postProcessModel(TheoryModel* m) {}
//--------------------------------- end collect model info
//--------------------------------- preprocessing
*/
virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {}
- enum PPAssertStatus {
+ enum PPAssertStatus
+ {
/** Atom has been solved */
PP_ASSERT_STATUS_SOLVED,
/** Atom has not been solved */
* NOTE: The presolve property must be added to the kinds file for
* the theory.
*/
- virtual void presolve() { }
+ virtual void presolve() {}
/**
* A Theory is called with postsolve exactly one time per user
* cannot raise conflicts, add lemmas, or propagate literals during
* postsolve().
*/
- virtual void postsolve() { }
+ virtual void postsolve() {}
/**
* Notification sent to the theory wheneven the search restarts.
* assume you're at DL 0 for the purposes of Contexts. This function
* should not use the output channel.
*/
- virtual void notifyRestart() { }
+ virtual void notifyRestart() {}
/**
* Identify this theory (for debugging, dynamic configuration,
*
* @return the iterator to the beginning of the fact queue
*/
- assertions_iterator facts_begin() const {
- return d_facts.begin();
- }
+ assertions_iterator facts_begin() const { return d_facts.begin(); }
/**
* Provides access to the facts queue, primarily intended for theory
*
* @return the iterator to the end of the fact queue
*/
- assertions_iterator facts_end() const {
- return d_facts.end();
- }
+ assertions_iterator facts_end() const { return d_facts.end(); }
/**
* Whether facts have been asserted to this theory.
*
bool hasFacts() { return !d_facts.empty(); }
/** Return total number of facts asserted to this theory */
- size_t numAssertions() {
- return d_facts.size();
- }
+ size_t numAssertions() { return d_facts.size(); }
typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
*
* @return the iterator to the beginning of the shared terms list
*/
- shared_terms_iterator shared_terms_begin() const {
+ shared_terms_iterator shared_terms_begin() const
+ {
return d_sharedTerms.begin();
}
*
* @return the iterator to the end of the shared terms list
*/
- shared_terms_iterator shared_terms_end() const {
- return d_sharedTerms.end();
- }
-
+ shared_terms_iterator shared_terms_end() const { return d_sharedTerms.end(); }
/**
- * This is a utility function for constructing a copy of the currently shared terms
- * in a queriable form. As this is
+ * This is a utility function for constructing a copy of the currently
+ * shared terms in a queriable form. As this is
*/
std::unordered_set<TNode> currentlySharedTerms() const;
* This allows the theory to be queried for whether a literal, lit, is
* entailed by the theory. This returns a pair of a Boolean and a node E.
*
- * If the Boolean is true, then E is a formula that entails lit and E is propositionally
- * entailed by the assertions to the theory.
+ * If the Boolean is true, then E is a formula that entails lit and E is
+ * propositionally entailed by the assertions to the theory.
*
* If the Boolean is false, it is "unknown" if lit is entailed and E may be
* any node.
*
- * The literal lit is either an atom a or (not a), which must belong to the theory:
- * There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
+ * The literal lit is either an atom a or (not a), which must belong to the
+ * theory: There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) ==
+ * this->getId().
*
* There are NO assumptions that a or the subterms of a have been
* preprocessed in any form. This includes ppRewrite, rewriting,
*
* Theories are free to limit the amount of effort they use and so may
* always opt to return "unknown". Both "unknown" and "not entailed",
- * may return for E a non-boolean Node (e.g. Node::null()). (There is no explicit output
- * for the negation of lit is entailed.)
+ * may return for E a non-boolean Node (e.g. Node::null()). (There is no
+ * explicit output for the negation of lit is entailed.)
*
* If lit is theory valid, the return result may be the Boolean constant
* true for E.
*
* If lit is entailed by multiple assertions on the theory's getFact()
* queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
- * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
+ * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ...
+ * a_k)
*
* If lit is entailed by a single assertion on the theory's getFact()
* queue, say a, this may return E=a.
* Theories may not touch their output stream during an entailment check.
*
* @param lit a literal belonging to the theory.
- * @return a pair <b,E> s.t. if b is true, then a formula E such that
- * E |= lit in the theory.
+ * @return a pair <b,E> s.t. if b is true, then a formula E such
+ * that E |= lit in the theory.
*/
virtual std::pair<bool, Node> entailmentCheck(TNode lit);
static bool usesCentralEqualityEngine(TheoryId id);
/** Explains/propagates via central equality engine only */
static bool expUsingCentralEqualityEngine(TheoryId id);
-};/* class Theory */
+}; /* class Theory */
std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
projects / cvc5.git / commitdiff