diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-17 17:07:14 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-17 17:07:14 +0200 |
commit | 83f4a3a884f53fa02019d1dab308240f0027c908 (patch) | |
tree | 2b6fd328ae243728e2d4f5be7ca129dd6bae2ebc /src/theory/quantifiers/conjecture_generator.h | |
parent | 36ac67d4eac45add325fbb2692569e4a781423a1 (diff) |
Refactor entailment filtering for conjecture generator. Other minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.h')
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.h | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 522a6420f..b0f25bd64 100755 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -294,6 +294,7 @@ private: //information regarding the conjectures /** list of all waiting conjectures */
std::vector< Node > d_waiting_conjectures_lhs;
std::vector< Node > d_waiting_conjectures_rhs;
+ std::vector< int > d_waiting_conjectures_score;
/** map of currently considered equality conjectures */
std::map< Node, std::vector< Node > > d_waiting_conjectures;
/** map of equality conjectures */
@@ -344,7 +345,7 @@ public: //term generation environment
TermGenEnv d_tge;
//consider term canon
- bool considerCurrentTermCanon( Node ln, bool genRelevant );
+ bool considerTermCanon( Node ln, bool genRelevant );
public: //for generalization
//generalizations
bool isGeneralization( TNode patg, TNode pat ) {
@@ -357,8 +358,8 @@ public: //for generalization public: //for property enumeration
//process this candidate conjecture
void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
- //whether it should be considered
- bool considerCandidateConjecture( TNode lhs, TNode rhs );
+ //whether it should be considered, negative : no, positive returns score
+ int considerCandidateConjecture( TNode lhs, TNode rhs );
//notified of a substitution
bool notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs );
//confirmation count
@@ -388,6 +389,8 @@ private: //information about ground equivalence classes bool isGroundTerm( TNode n );
// count of full effort checks
unsigned d_fullEffortCount;
+ //flush the waiting conjectures
+ unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
public:
ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
/* needs check */
@@ -405,12 +408,8 @@ public: //options
private:
bool optReqDistinctVarPatterns();
- bool optFilterFalsification();
bool optFilterUnknown();
- bool optFilterConfirmation();
- unsigned optFilterConfirmationDomainThreshold();
- bool optFilterConfirmationOnlyGround();
- bool optFilterConfirmationNonCanonical(); //filter if all ground confirmations are non-canonical
+ int optFilterScoreThreshold();
unsigned optFullCheckFrequency();
unsigned optFullCheckConjectures();
|