diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-12 16:46:51 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-12 16:46:51 +0000 |
commit | 0ba075e240b2083163ab35a3580547cae6927b6c (patch) | |
tree | 47be765d608aff213ee58749adab458f315fcf89 /src/theory/rep_set.h | |
parent | 341794b1cbd5693010c78b9f5bfe232ee90404b0 (diff) |
minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 8e7da4ce5..61b2ebf9f 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -54,14 +54,14 @@ typedef std::vector< int > RepDomain; class RepSetIterator {
private:
//initialize function
- void initialize();
+ bool initialize();
public:
RepSetIterator( RepSet* rs );
~RepSetIterator(){}
//set that this iterator will be iterating over instantiations for a quantifier
- void setQuantifier( Node f );
+ bool setQuantifier( Node f );
//set that this iterator will be iterating over the domain of a function
- void setFunctionDomain( Node op );
+ bool setFunctionDomain( Node op );
public:
//pointer to model
RepSet* d_rep_set;
|