diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-13 11:22:43 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-13 11:22:43 -0500 |
commit | decde5be0b6409b9c1b84f40c8383bb8483e4566 (patch) | |
tree | 0130bf76dde48a28fc68dcc14e61c2b9fabc923c /src/theory/quantifiers/conjecture_generator.cpp | |
parent | dd01099518aab8d42d788dfadadbe11763ec9d18 (diff) |
Handle parametric datatypes with --quant-ind. Minor updates.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 27bbb0f5f..2cc49ef5a 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -605,7 +605,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { std::vector< TypeNode > rt_types; std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs; unsigned addedLemmas = 0; - for( unsigned depth=1; depth<=3; depth++ ){ + unsigned maxDepth = options::conjectureGenMaxDepth(); + for( unsigned depth=1; depth<=maxDepth; depth++ ){ Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl; Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl; //set up environment @@ -1167,6 +1168,8 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi d_waiting_conjectures_score.push_back( score ); d_waiting_conjectures[lhs].push_back( rhs ); d_waiting_conjectures[rhs].push_back( lhs ); + }else{ + Trace("sg-conjecture-debug2") << "...do not consider " << lhs << " == " << rhs << ", score = " << score << std::endl; } } |