diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-11 17:36:07 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-11 17:36:07 -0500 |
commit | 24d60fa5654a32b09dc8de79b7704fbf40051478 (patch) | |
tree | d3bce397adceb1407764a54489c191aea06d134a /src/theory/rep_set.h | |
parent | f6d24c56905449e68ee23a9cea54985eacd24aa3 (diff) |
Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 24fa7473e..b92d9d2c6 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -23,6 +23,8 @@ namespace CVC4 { namespace theory { +class QuantifiersEngine; + /** this class stores a representative set */ class RepSet { public: @@ -53,15 +55,26 @@ typedef std::vector< int > RepDomain; /** this class iterates over a RepSet */ class RepSetIterator { private: + enum { + ENUM_DOMAIN_ELEMENTS, + ENUM_RANGE, + }; + //initialize function - bool initialize(); + bool initialize(QuantifiersEngine * qe, Node f); + //enumeration type? + std::vector< int > d_enum_type; + //for enum ranges + std::map< int, Node > d_lower_bounds; + //domain size + int domainSize( int i ); public: RepSetIterator( RepSet* rs ); ~RepSetIterator(){} //set that this iterator will be iterating over instantiations for a quantifier - bool setQuantifier( Node f ); + bool setQuantifier( QuantifiersEngine * qe, Node f ); //set that this iterator will be iterating over the domain of a function - bool setFunctionDomain( Node op ); + bool setFunctionDomain( QuantifiersEngine * qe, Node op ); public: //pointer to model RepSet* d_rep_set; @@ -90,7 +103,7 @@ public: /** set index order */ void setIndexOrder( std::vector< int >& indexOrder ); /** set domain */ - void setDomain( std::vector< RepDomain >& domain ); + //void setDomain( std::vector< RepDomain >& domain ); /** increment the iterator at index=counter */ void increment2( int counter ); /** increment the iterator */ |