From aa8da1ff4e7f119408dbf14074b9a5efcb06618b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 18 Aug 2020 15:52:30 -0500 Subject: [PATCH] Introduce the theory state object (#4910) This will be used as a standard way of querying and tracking state information in a Theory. The TheoryState object has a standard role in a number of the new standard templates for Theory:: methods. The theory state is a collection of 4 Theory members (SAT context, user context, valuation, equality engine), as well as a SAT-context dependent "conflict" flag that indicates whether we have sent a conflict in this SAT conflict. It contains (safe) versions of equality engine queries, which are highly common in many theory solvers. The next step will be to have the SolverState objects in theory of sets and strings inherit from this class. --- src/CMakeLists.txt | 2 + src/theory/theory.cpp | 1 + src/theory/theory.h | 6 ++ src/theory/theory_state.cpp | 129 ++++++++++++++++++++++++++++++++++++ src/theory/theory_state.h | 94 ++++++++++++++++++++++++++ 5 files changed, 232 insertions(+) create mode 100644 src/theory/theory_state.cpp create mode 100644 src/theory/theory_state.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 10cf23fdf..48bd99f44 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -818,6 +818,8 @@ libcvc4_add_sources( theory/theory_rewriter.cpp theory/theory_rewriter.h theory/theory_registrar.h + theory/theory_state.cpp + theory/theory_state.h theory/theory_test_utils.h theory/trust_node.cpp theory/trust_node.h diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 02f84526f..9669d97e0 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -82,6 +82,7 @@ Theory::Theory(TheoryId id, d_valuation(valuation), d_equalityEngine(nullptr), d_allocEqualityEngine(nullptr), + d_theoryState(nullptr), d_proofsEnabled(false) { smtStatisticsRegistry()->registerStat(&d_checkTime); diff --git a/src/theory/theory.h b/src/theory/theory.h index 78c6e34cb..349f36a57 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -44,6 +44,7 @@ #include "theory/output_channel.h" #include "theory/theory_id.h" #include "theory/theory_rewriter.h" +#include "theory/theory_state.h" #include "theory/trust_node.h" #include "theory/valuation.h" #include "util/statistics_registry.h" @@ -267,6 +268,11 @@ class Theory { * The official equality engine, if we allocated it. */ std::unique_ptr d_allocEqualityEngine; + /** + * The theory state, which contains contexts, valuation, and equality engine. + * Notice the theory is responsible for memory management of this class. + */ + TheoryState* d_theoryState; /** * Whether proofs are enabled * diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp new file mode 100644 index 000000000..bc8e53245 --- /dev/null +++ b/src/theory/theory_state.cpp @@ -0,0 +1,129 @@ +/********************* */ +/*! \file theory_state.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A theory state for Theory + **/ + +#include "theory/theory_state.h" + +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +TheoryState::TheoryState(context::Context* c, + context::UserContext* u, + Valuation val) + : d_context(c), + d_ucontext(u), + d_valuation(val), + d_ee(nullptr), + d_conflict(c, false) +{ +} + +void TheoryState::finishInit(eq::EqualityEngine* ee) { d_ee = ee; } + +context::Context* TheoryState::getSatContext() const { return d_context; } + +context::UserContext* TheoryState::getUserContext() const { return d_ucontext; } + +bool TheoryState::hasTerm(TNode a) const +{ + Assert(d_ee != nullptr); + return d_ee->hasTerm(a); +} + +TNode TheoryState::getRepresentative(TNode t) const +{ + Assert(d_ee != nullptr); + if (d_ee->hasTerm(t)) + { + return d_ee->getRepresentative(t); + } + return t; +} + +bool TheoryState::areEqual(TNode a, TNode b) const +{ + Assert(d_ee != nullptr); + if (a == b) + { + return true; + } + else if (hasTerm(a) && hasTerm(b)) + { + return d_ee->areEqual(a, b); + } + return false; +} + +bool TheoryState::areDisequal(TNode a, TNode b) const +{ + Assert(d_ee != nullptr); + if (a == b) + { + return false; + } + + bool isConst = true; + bool hasTerms = true; + if (hasTerm(a)) + { + a = d_ee->getRepresentative(a); + isConst = a.isConst(); + } + else if (!a.isConst()) + { + // if not constant and not a term in the ee, it cannot be disequal + return false; + } + else + { + hasTerms = false; + } + + if (hasTerm(b)) + { + b = d_ee->getRepresentative(b); + isConst = isConst && b.isConst(); + } + else if (!b.isConst()) + { + // same as above, it cannot be disequal + return false; + } + else + { + hasTerms = false; + } + + if (isConst) + { + // distinct constants are disequal + return a != b; + } + else if (!hasTerms) + { + return false; + } + // otherwise there may be an explicit disequality in the equality engine + return d_ee->areDisequal(a, b, false); +} + +eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; } + +void TheoryState::notifyInConflict() { d_conflict = true; } + +bool TheoryState::isInConflict() const { return d_conflict; } + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h new file mode 100644 index 000000000..71197dddc --- /dev/null +++ b/src/theory/theory_state.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file theory_state.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A theory state for Theory + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__THEORY_STATE_H +#define CVC4__THEORY__THEORY_STATE_H + +#include "context/cdo.h" +#include "expr/node.h" +#include "theory/valuation.h" + +namespace CVC4 { +namespace theory { + +namespace eq { +class EqualityEngine; +} + +class TheoryState +{ + public: + TheoryState(context::Context* c, context::UserContext* u, Valuation val); + virtual ~TheoryState() {} + /** + * Finish initialize, ee is a pointer to the official equality engine + * of theory. + */ + virtual void finishInit(eq::EqualityEngine* ee); + /** Get the SAT context */ + context::Context* getSatContext() const; + /** Get the user context */ + context::UserContext* getUserContext() const; + //-------------------------------------- equality information + /** Is t registered as a term in the equality engine of this class? */ + virtual bool hasTerm(TNode a) const; + /** + * Get the representative of t in the equality engine of this class, or t + * itself if it is not registered as a term. + */ + virtual TNode getRepresentative(TNode t) const; + /** + * Are a and b equal according to the equality engine of this class? Also + * returns true if a and b are identical. + */ + virtual bool areEqual(TNode a, TNode b) const; + /** + * Are a and b disequal according to the equality engine of this class? Also + * returns true if the representative of a and b are distinct constants. + */ + virtual bool areDisequal(TNode a, TNode b) const; + /** get equality engine */ + eq::EqualityEngine* getEqualityEngine() const; + //-------------------------------------- end equality information + /** + * Set that the current state of the solver is in conflict. This should be + * called immediately after a call to conflict(...) on the output channel of + * the theory. + */ + virtual void notifyInConflict(); + /** Are we currently in conflict? */ + virtual bool isInConflict() const; + + protected: + /** Pointer to the SAT context object used by the theory. */ + context::Context* d_context; + /** Pointer to the user context object used by the theory. */ + context::UserContext* d_ucontext; + /** + * The valuation proxy for the Theory to communicate back with the + * theory engine (and other theories). + */ + Valuation d_valuation; + /** Pointer to equality engine of the theory. */ + eq::EqualityEngine* d_ee; + /** Are we in conflict? */ + context::CDO d_conflict; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__SOLVER_STATE_H */ -- 2.30.2