diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-03 17:23:04 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-03 17:23:04 +0200 |
commit | ec2a8ad5e5be550f4f0c5c3be92ee20bf2977efa (patch) | |
tree | 6df6b309d0e85a2ab56a293c1849be8b2988044e /src/theory/quantifiers/conjecture_generator.h | |
parent | 83f91b92090ef0231156560f337affc6e5c2a33f (diff) |
Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for relevant term filtering.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.h')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 94a13829c..93cda7311 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -85,10 +85,10 @@ public: //match status
int d_match_status;
int d_match_status_child_num;
- //match mode
- //1 : different variables must have different matches
- //2 : variables must map to ground terms
- //3 : both 1 and 2
+ //match mode bits
+ //0 : different variables must have different matches
+ //1 : variables must map to ground terms
+ //2 : variables must map to non-ground terms
unsigned d_match_mode;
//children
std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;
@@ -312,7 +312,6 @@ public: //for generalization return isGeneralization( patg, pat, subs );
}
bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );
-
public: //for property enumeration
//process this candidate conjecture
void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
|