From d38d41b3f3604fc728ec71499d1f3af3dfb46ccd Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 24 Sep 2014 16:42:31 +0200 Subject: [PATCH] Fix infinite loop in datatypes enumerator. Minor work on conjecture generator. --- src/theory/datatypes/type_enumerator.h | 29 +----- .../quantifiers/conjecture_generator.cpp | 95 +++++++++++++------ src/theory/quantifiers/conjecture_generator.h | 10 +- test/regress/regress0/datatypes/Makefile.am | 3 +- .../regress/regress0/datatypes/tenum-bug.smt2 | 11 +++ 5 files changed, 91 insertions(+), 57 deletions(-) create mode 100644 test/regress/regress0/datatypes/tenum-bug.smt2 diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 256dcaef2..a514460c7 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -75,31 +75,10 @@ public: Debug("te") << "datatype is kind " << type.getKind() << std::endl; Debug("te") << "datatype is " << type << std::endl; - /* find the "zero" constructor (the first non-recursive one) */ - /* FIXME: this isn't sufficient for mutually-recursive datatypes! */ - while(d_zeroCtor < d_datatype.getNumConstructors()) { - bool recursive = false; - if( d_datatype.isParametric() ){ - TypeNode tn = TypeNode::fromType( d_datatype[d_zeroCtor].getSpecializedConstructorType(d_type.toType()) ); - for( unsigned i=0; i Total LHS of depth : " << rel_term_count << std::endl; + Trace("sg-stats") << "--------> Total LHS of depth " << depth << " : " << rel_term_count << std::endl; //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl; - //now generate right hand sides + + /* test... + for( unsigned i=0; i=options::conjectureGenPerRound() ){ + break; + } } if( (int)addedLemmas>=options::conjectureGenPerRound() ){ break; @@ -825,13 +837,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { TNode r = (*ueqcs_i); bool firstTime = true; TNode rr = getUniversalRepresentative( r ); - Trace("thm-ee") << " " << r; - if( rr!=r ){ Trace("thm-ee") << " [" << rr << "]"; } + Trace("thm-ee") << " " << rr; Trace("thm-ee") << " : { "; eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine ); while( !ueqc_i.isFinished() ){ TNode n = (*ueqc_i); - if( r!=n ){ + if( rr!=n ){ if( firstTime ){ Trace("thm-ee") << std::endl; firstTime = false; @@ -879,32 +890,36 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in //we have determined a relevant subgoal Node lhs = d_waiting_conjectures_lhs[indices[i]]; Node rhs = d_waiting_conjectures_rhs[indices[i]]; - Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl; - Trace("sg-engine-debug") << " score : " << d_waiting_conjectures_score[indices[i]] << std::endl; - std::vector< Node > bvs; - for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){ - for( unsigned i=0; i<=it->second; i++ ){ - bvs.push_back( getFreeVar( it->first, i ) ); - } - } - Node rsg; - if( !bvs.empty() ){ - Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ); - rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) ); + if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){ + //skip }else{ - rsg = lhs.eqNode( rhs ); - } - rsg = Rewriter::rewrite( rsg ); - d_conjectures.push_back( rsg ); - d_eq_conjectures[lhs].push_back( rhs ); - d_eq_conjectures[rhs].push_back( lhs ); - - Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg ); - d_quantEngine->addLemma( lem, false ); - d_quantEngine->addRequirePhase( rsg, false ); - addedLemmas++; - if( (int)addedLemmas>=options::conjectureGenPerRound() ){ - break; + Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl; + Trace("sg-engine-debug") << " score : " << d_waiting_conjectures_score[indices[i]] << std::endl; + std::vector< Node > bvs; + for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){ + for( unsigned i=0; i<=it->second; i++ ){ + bvs.push_back( getFreeVar( it->first, i ) ); + } + } + Node rsg; + if( !bvs.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ); + rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) ); + }else{ + rsg = lhs.eqNode( rhs ); + } + rsg = Rewriter::rewrite( rsg ); + d_conjectures.push_back( rsg ); + d_eq_conjectures[lhs].push_back( rhs ); + d_eq_conjectures[rhs].push_back( lhs ); + + Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg ); + d_quantEngine->addLemma( lem, false ); + d_quantEngine->addRequirePhase( rsg, false ); + addedLemmas++; + if( (int)addedLemmas>=options::conjectureGenPerRound() ){ + break; + } } }else{ if( doSort ){ @@ -1059,6 +1074,26 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo } } +Node ConjectureGenerator::getEnumerateTerm( TypeNode tn, unsigned index ) { + std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); + unsigned teIndex; + if( it==d_typ_enum_map.end() ){ + teIndex = (int)d_typ_enum.size(); + d_typ_enum_map[tn] = teIndex; + d_typ_enum.push_back( TypeEnumerator(tn) ); + }else{ + teIndex = it->second; + } + while( index>=d_enum_terms[tn].size() ){ + if( d_typ_enum[teIndex].isFinished() ){ + return Node::null(); + } + d_enum_terms[tn].push_back( *d_typ_enum[teIndex] ); + ++d_typ_enum[teIndex]; + } + return d_enum_terms[tn][index]; +} + void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) { int score = considerCandidateConjecture( lhs, rhs ); if( score>0 ){ diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index b0f25bd64..eb7f4b2aa 100755 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -20,6 +20,7 @@ #include "context/cdhashmap.h" #include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" +#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { @@ -355,6 +356,14 @@ public: //for generalization bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs ); // get generalization depth int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ); +private: + //ground term enumeration + std::map< TypeNode, std::vector< Node > > d_enum_terms; + //type enumerators + std::map< TypeNode, unsigned > d_typ_enum_map; + std::vector< TypeEnumerator > d_typ_enum; + //get nth term for type + Node getEnumerateTerm( TypeNode tn, unsigned index ); public: //for property enumeration //process this candidate conjecture void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ); @@ -404,7 +413,6 @@ public: void assertNode( Node n ); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "ConjectureGenerator"; } - //options private: bool optReqDistinctVarPatterns(); diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index e8a8f16f5..a3a984682 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -58,7 +58,8 @@ TESTS = \ bug286.cvc \ bug438.cvc \ bug438b.cvc \ - wrong-sel-simp.cvc + wrong-sel-simp.cvc \ + tenum-bug.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/tenum-bug.smt2 b/test/regress/regress0/datatypes/tenum-bug.smt2 new file mode 100644 index 000000000..bf82c7b8c --- /dev/null +++ b/test/regress/regress0/datatypes/tenum-bug.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status sat) + +(declare-datatypes () ((DNat (dnat (data Nat))) + (Nat (succ (pred DNat)) (zero)))) + +(declare-fun x () Nat) + +(assert (not (= x zero))) + +(check-sat) \ No newline at end of file -- 2.30.2