From aa3b60104a0026c078eea1d19506e8bf4c3d9763 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 May 2014 16:59:48 -0500 Subject: [PATCH] Fix bug in E-matching Real/Int terms. --- proofs/lfsc_checker/check.cpp | 2 +- src/theory/quantifiers/candidate_generator.cpp | 4 ++-- src/theory/quantifiers/inst_match_generator.cpp | 6 ++++-- src/theory/quantifiers/term_database.cpp | 17 +++++++++++++++++ src/theory/quantifiers/term_database.h | 1 + test/regress/regress0/quantifiers/Makefile.am | 3 ++- .../regress0/quantifiers/simp-typ-test.smt2 | 7 +++++++ 7 files changed, 34 insertions(+), 6 deletions(-) create mode 100755 test/regress/regress0/quantifiers/simp-typ-test.smt2 diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp index b550c58a1..c96791aeb 100644 --- a/proofs/lfsc_checker/check.cpp +++ b/proofs/lfsc_checker/check.cpp @@ -61,7 +61,7 @@ void report_error(const string &msg) { not_defeq2->print(cout); } cout.flush(); - _exit(1); + exit(1); } Expr *call_run_code(Expr *code) { diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 9b5e506ea..799513171 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -175,7 +175,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){ while( !d_eq.isFinished() ){ Node n = (*d_eq); ++d_eq; - if( n.getType()==d_match_pattern[0].getType() ){ + if( n.getType().isSubtypeOf( d_match_pattern[0].getType() ) ){ //an equivalence class with the same type as the pattern, return reflexive equality return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); } @@ -228,7 +228,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { while( !d_eq.isFinished() ){ Node n = (*d_eq); ++d_eq; - if( n.getType()==d_match_pattern.getType() ){ + if( n.getType().isSubtypeOf( d_match_pattern.getType() ) ){ //an equivalence class with the same type as the pattern, return it return n; } diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index da0a3c4f6..9031104c8 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -32,6 +32,7 @@ namespace inst { InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){ + d_needsReset = true; d_active_add = false; Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); d_pattern = pat; @@ -298,7 +299,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* t = d_cg->getNextCandidate(); Trace("matching-debug2") << "Matching candidate : " << t << std::endl; //if t not null, try to fit it into match m - if( !t.isNull() && t.getType()==d_match_pattern.getType() ){ + if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern.getType() ) ){ success = getMatch( f, t, m, qe ); } }while( !success && !t.isNull() ); @@ -628,6 +629,7 @@ int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, Q } void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){ + Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; if( argIndex==(int)d_match_pattern.getNumChildren() ){ //m is an instantiation if( qe->addInstantiation( d_f, m ) ){ @@ -640,7 +642,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ Node t = it->first; Node prev = m.get( v ); - if( ( prev.isNull() || prev==t ) && d_match_pattern[argIndex].getType()==t.getType() ){ + if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern[argIndex].getType() ) ){ m.setValue( v, t); addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); m.setValue( v, prev); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 64965f5ce..36859ddaa 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -48,6 +48,14 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ } } +void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { + for( std::map< Node, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + for( unsigned i=0; ifirst << std::endl; + it->second.debugPrint( c, n, depth+1 ); + } +} + TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) { } @@ -204,6 +212,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Debug("term-db-cong") << "TermDb: Reset" << std::endl; Debug("term-db-cong") << "Congruent/Non-Congruent = "; Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl; + if( Debug.isOn("term-db") ){ + Debug("term-db") << "functions : " << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ + if( it->second.size()>0 ){ + Debug("term-db") << "- " << it->first << std::endl; + d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]); + } + } + } } Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 2a72cf808..2592e1fd6 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -76,6 +76,7 @@ public: std::map< Node, TermArgTrie > d_data; public: bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } + void debugPrint( const char * c, Node n, unsigned depth = 0 ); };/* class TermArgTrie */ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index e399b4b23..7e8e1ea99 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -42,7 +42,8 @@ TESTS = \ symmetric_unsat_7.smt2 \ javafe.ast.StmtVec.009.smt2 \ ARI176e1.smt2 \ - bi-artm-s.smt2 + bi-artm-s.smt2 \ + simp-typ-test.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/simp-typ-test.smt2 b/test/regress/regress0/quantifiers/simp-typ-test.smt2 new file mode 100755 index 000000000..366559b9d --- /dev/null +++ b/test/regress/regress0/quantifiers/simp-typ-test.smt2 @@ -0,0 +1,7 @@ +(set-logic UFLIRA) +(set-info :status unsat) +; ensure that E-matching matches on sub-types +(declare-fun P (Real) Bool) +(assert (forall ((x Real)) (P x))) +(assert (not (P 5))) +(check-sat) \ No newline at end of file -- 2.30.2