From ec2a8ad5e5be550f4f0c5c3be92ee20bf2977efa Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 3 Sep 2014 17:23:04 +0200 Subject: Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for relevant term filtering. --- src/theory/quantifiers/conjecture_generator.h | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'src/theory/quantifiers/conjecture_generator.h') 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 ); -- cgit v1.2.3