diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 11:20:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-27 11:20:50 -0500 |
commit | 079ed9540d498bcbb58f2f0fbe87bdae28101d1e (patch) | |
tree | 8c3ba1818dc515c1714b23555460a3a39192acc5 /src/theory/rep_set.h | |
parent | 03cc40cc070df0bc11c1556cef3016f784a95d23 (diff) |
Refactor theory model (#1236)
* Refactor theory model, working on making RepSet references const.
* Encapsulation of members of rep set.
* More documentation on rep set.
* Swap names
* Reference issues.
* Minor
* Minor
* New clang format.
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 83 |
1 files changed, 70 insertions, 13 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 41044b526..a20e56184 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -17,40 +17,97 @@ #ifndef __CVC4__THEORY__REP_SET_H #define __CVC4__THEORY__REP_SET_H -#include "expr/node.h" #include <map> +#include <vector> + +#include "expr/node.h" +#include "expr/type_node.h" namespace CVC4 { namespace theory { class QuantifiersEngine; -/** this class stores a representative set */ +/** representative set + * + * This class contains finite lists of values for types, typically values and + * types that exist + * in the equality engine of a model object. In the following, "representative" + * means a value that exists in this set. + * + * This class is used for finite model finding and other exhaustive + * instantiation-based + * methods. The class goes beyond just maintaining a list of values that occur + * in the equality engine in the following ways: + + * (1) It maintains a partial mapping from representatives to a term that has + * that value in the current + * model. This is important because algorithms like the instantiation method in + * Reynolds et al CADE 2013 + * act on "term models" where domains in models are interpreted as a set of + * representative terms. Hence, + * instead of instantiating with e.g. uninterpreted constants u, we instantiate + * with the corresponding term that is interpreted as u. + + * (2) It is mutable, calls to add(...) and complete(...) may modify this class + * as necessary, for instance + * in the case that there are no ground terms of a type that occurs in a + * quantified formula, or for + * exhaustive instantiation strategies that enumerate over small interpreted + * finite types. + */ class RepSet { public: RepSet(){} ~RepSet(){} + /** map from types to the list of representatives + * TODO : as part of #1199, encapsulate this + */ std::map< TypeNode, std::vector< Node > > d_type_reps; - std::map< TypeNode, bool > d_type_complete; - std::map< Node, int > d_tmap; - // map from values to terms they were assigned for - std::map< Node, Node > d_values_to_terms; /** clear the set */ void clear(); - /** has type */ + /** does this set have representatives of type tn? */ bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); } - /** has rep */ - bool hasRep( TypeNode tn, Node n ); - /** get cardinality for type */ - int getNumRepresentatives( TypeNode tn ) const; - /** add representative for type */ + /** does this set have representative n of type tn? */ + bool hasRep(TypeNode tn, Node n) const; + /** get the number of representatives for type */ + unsigned getNumRepresentatives(TypeNode tn) const; + /** get representative at index */ + Node getRepresentative(TypeNode tn, unsigned i) const; + /** add representative n for type tn, where n has type tn */ void add( TypeNode tn, Node n ); /** returns index in d_type_reps for node n */ int getIndexFor( Node n ) const; - /** complete all values */ + /** complete the list for type t + * Resets d_type_reps[tn] and repopulates by running the type enumerator for + * that type exhaustively. + * This should only be called for small finite interpreted types. + */ bool complete( TypeNode t ); + /** get term for representative + * Returns a term that is interpreted as representative n in the current + * model, null otherwise. + */ + Node getTermForRepresentative(Node n) const; + /** set term for representative + * Called when t is interpreted as value n. Subsequent class to + * getTermForRepresentative( n ) will return t. + */ + void setTermForRepresentative(Node n, Node t); + /** get existing domain value, with possible exclusions + * This function returns a term in d_type_reps[tn] but not in exclude + */ + Node getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const; /** debug print */ void toStream(std::ostream& out); + + private: + /** whether the list of representatives for types are complete */ + std::map<TypeNode, bool> d_type_complete; + /** map from representatives to their index in d_type_reps */ + std::map<Node, int> d_tmap; + /** map from values to terms they were assigned for */ + std::map<Node, Node> d_values_to_terms; };/* class RepSet */ //representative domain |