diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-08 10:14:31 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-08 10:14:31 -0600 |
commit | 564234963dd7e76c8d9b88ef941a6683694e5b53 (patch) | |
tree | 313e46520c07d1536fffbad4b7080937cfc09aae /src/theory/theory_model.h | |
parent | 805d4b7483e51a9b4d24058d493f85700a87f099 (diff) |
Make collect model info return a Bool (#1421)
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 77 |
1 files changed, 57 insertions, 20 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 600f511c8..ab844c6ec 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -55,19 +55,25 @@ namespace theory { * * These calls may modify the model object using the interface * functions below, including: - * - assertEquality, assertPredicate, assertRepresentative, + * - assertEquality, assertPredicate, assertSkeleton, * assertEqualityEngine. * - assignFunctionDefinition * - * During and after this building process, these calls may use - * interface functions below to guide the model construction: + * This class provides several interface functions: * - hasTerm, getRepresentative, areEqual, areDisequal * - getEqualityEngine * - getRepSet * - hasAssignedFunctionDefinition, getFunctionsToAssign + * - getValue * - * After this building process, the function getValue can be - * used to query the value of nodes. + * The above functions can be used for a model m after it has been + * successfully built, i.e. when m->isBuiltSuccess() returns true. + * + * Additionally, all of the above functions, with the exception of getValue, + * can be used during step (5) of TheoryEngineModelBuilder::buildModel, as + * documented in theory_model_builder.h. In particular, we make calls to the + * above functions such as getRepresentative() when assigning total + * interpretations for uninterpreted functions. */ class TheoryModel : public Model { @@ -80,7 +86,7 @@ public: virtual void reset(); /** is built * - * Have we (attempted to) build this model since the last + * Have we attempted to build this model since the last * call to reset? Notice for model building techniques * that are not guaranteed to succeed (such as * when quantified formulas are enabled), a true return @@ -88,22 +94,51 @@ public: * current assertions. */ bool isBuilt() { return d_modelBuilt; } + /** is built success + * + * Was this model successfully built since the last call to reset? + */ + bool isBuiltSuccess() { return d_modelBuiltSuccess; } //---------------------------- for building the model /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); - /** assert equality holds in the model */ - void assertEquality(TNode a, TNode b, bool polarity); - /** assert predicate holds in the model */ - void assertPredicate(TNode a, bool polarity); - /** assert all equalities/predicates in equality engine hold in the model */ - void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL); - /** assert representative - * This function tells the model that n should be the representative of its equivalence class. - * It should be called during model generation, before final representatives are chosen. In the - * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... ) - * functions. - */ - void assertRepresentative(TNode n); + /** assert equality holds in the model + * + * This method returns true if and only if the equality engine of this model + * is consistent after asserting the equality to this model. + */ + bool assertEquality(TNode a, TNode b, bool polarity); + /** assert predicate holds in the model + * + * This method returns true if and only if the equality engine of this model + * is consistent after asserting the predicate to this model. + */ + bool assertPredicate(TNode a, bool polarity); + /** assert all equalities/predicates in equality engine hold in the model + * + * This method returns true if and only if the equality engine of this model + * is consistent after asserting the equality engine to this model. + */ + bool assertEqualityEngine(const eq::EqualityEngine* ee, + std::set<Node>* termSet = NULL); + /** assert skeleton + * + * This method gives a "skeleton" for the model value of the equivalence + * class containing n. This should be an application of interpreted function + * (e.g. datatype constructor, array store, set union chain). The subterms of + * this term that are variables or terms that belong to other theories will + * be filled in with model values. + * + * For example, if we call assertSkeleton on (C x y) where C is a datatype + * constructor and x and y are variables, then the equivalence class of + * (C x y) will be interpreted in m as (C x^m y^m) where + * x^m = m->getValue( x ) and y^m = m->getValue( y ). + * + * It should be called during model generation, before final representatives + * are chosen. In the case of TheoryEngineModelBuilder, it should be called + * during Theory's collectModelInfo( ... ) functions. + */ + void assertSkeleton(TNode n); //---------------------------- end building the model // ------------------- general equality queries @@ -171,8 +206,10 @@ public: protected: /** substitution map for this model */ SubstitutionMap d_substitutions; - /** whether this model has been built */ + /** whether we have tried to build this model in the current context */ bool d_modelBuilt; + /** whether this model has been built successfully */ + bool d_modelBuiltSuccess; /** special local context for our equalityEngine so we can clear it * independently of search context */ context::Context* d_eeContext; |