From: ajreynol Date: Tue, 22 Mar 2016 19:07:21 +0000 (-0500) Subject: Bug fix for define functions + incremental. Minor work on relational triggers. X-Git-Tag: cvc5-1.0.0~6049^2~99 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0ee7aa783c299eca1127005b590dd157b315f130;p=cvc5.git Bug fix for define functions + incremental. Minor work on relational triggers. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5e97158ca..bbaa07af5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2123,6 +2123,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const void SmtEngine::defineFunction(Expr func, const std::vector& formals, Expr formula) { + SmtScope smts(this); + doPendingPops(); Trace("smt") << "SMT defineFunction(" << func << ")" << endl; for(std::vector::const_iterator i = formals.begin(); i != formals.end(); ++i) { if((*i).getKind() != kind::BOUND_VARIABLE) { @@ -2141,7 +2143,6 @@ void SmtEngine::defineFunction(Expr func, DefineFunctionCommand c(ss.str(), func, formals, formula); addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); - SmtScope smts(this); PROOF( if (options::checkUnsatCores()) { d_defineCommands.push_back(c.clone()); diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 680be77da..1f68884b6 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -130,21 +130,37 @@ Node CandidateGeneratorQE::getNextCandidate(){ CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : d_match_pattern( mpat ), d_qe( qe ){ - + Assert( mpat.getKind()==EQUAL ); + for( unsigned i=0; i<2; i++ ){ + if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){ + d_match_gterm = mpat[i]; + } + } } void CandidateGeneratorQELitEq::resetInstantiationRound(){ } void CandidateGeneratorQELitEq::reset( Node eqc ){ - d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + if( d_match_gterm.isNull() ){ + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + }else{ + d_do_mgt = true; + } } Node CandidateGeneratorQELitEq::getNextCandidate(){ - while( !d_eq.isFinished() ){ - Node n = (*d_eq); - ++d_eq; - if( n.getType().isComparableTo( 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 ); + if( d_match_gterm.isNull() ){ + while( !d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType().isComparableTo( 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 ); + } + } + }else{ + if( d_do_mgt ){ + d_do_mgt = false; + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm ); } } return Node::null(); diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index fb120dd08..d86891de7 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -108,6 +108,8 @@ private: eq::EqClassesIterator d_eq; //equality you are trying to match equalities for Node d_match_pattern; + Node d_match_gterm; + bool d_do_mgt; //einstantiator pointer QuantifiersEngine* d_qe; public: diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 621327c0b..111eab116 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -51,10 +51,12 @@ struct sortQuantifiersForSymbol { struct sortTriggers { bool operator() (Node i, Node j) { - if( Trigger::isAtomicTrigger( i ) ){ - return igetTermDatabase()->getInstConstantBody( f ); Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true ); Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; - for( int i=0; i<(int)patTermsF.size(); i++ ){ - Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl; - } - Trace("auto-gen-trigger-debug") << std::endl; if( ntrivTriggers ){ sortTriggers st; std::sort( patTermsF.begin(), patTermsF.end(), st ); } + for( unsigned i=0; i > varContains; std::map< Node, bool > vcMap; std::map< Node, bool > rmPatTermsF; + int last_weight = -1; for( unsigned i=0; igetTermDatabase()->getVarContainsNode( f, patTermsF[i], varContains[ patTermsF[i] ] ); bool newVar = false; @@ -279,9 +282,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ newVar = true; } } - if( ntrivTriggers && !newVar && !Trigger::isAtomicTrigger( patTermsF[i] ) ){ + int curr_w = Trigger::getTriggerWeight( patTermsF[i] ); + if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){ Trace("auto-gen-trigger-debug") << "Exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl; rmPatTermsF[patTermsF[i]] = true; + }else{ + last_weight = curr_w; } } for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 0628b7fbc..48385e28b 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -242,7 +242,7 @@ bool Trigger::isUsable( Node n, Node q ){ } Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { - Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl; + Trace("trigger-debug") << "Is " << n << " a usable trigger? pol/hasPol=" << pol << "/" << hasPol << std::endl; if( n.getKind()==NOT ){ pol = !pol; n = n[0]; @@ -254,7 +254,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { bool is_arith = n[0].getType().isReal(); for( unsigned i=0; i<2; i++) { if( n[1-i].getKind()==INST_CONSTANT ){ - if( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) && ( !do_negate || is_arith ) ){ + if( ( ( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ) || !quantifiers::TermDb::hasInstConstAttr(n[i]) ) && + ( !do_negate || is_arith ) ){ rtr = n; break; } @@ -274,7 +275,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { Node veq; if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){ int vti = veq[0]==it->first ? 1 : 0; - if( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ){ + if( ( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ) || !quantifiers::TermDb::hasInstConstAttr(veq[vti]) ){ rtr = veq; } } @@ -434,6 +435,23 @@ bool Trigger::isPureTheoryTrigger( Node n ) { } } +int Trigger::getTriggerWeight( Node n ) { + if( isAtomicTrigger( n ) ){ + return 0; + }else{ + if( options::relationalTriggers() ){ + if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ + for( unsigned i=0; i<2; i++ ){ + if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermDb::hasInstConstAttr( n[1-i] ) ){ + return 0; + } + } + } + } + return 1; + } +} + bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) { if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){ if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 11962008e..bbbf9495f 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -112,6 +112,7 @@ public: static bool isSimpleTrigger( Node n ); static bool isBooleanTermTrigger( Node n ); static bool isPureTheoryTrigger( Node n ); + static int getTriggerWeight( Node n ); static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ); /** return data structure for producing matches for this trigger. */ static InstMatchGenerator* getInstMatchGenerator( Node q, Node n ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4be55ebb5..754b0c224 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -88,6 +88,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_te( te ), d_lemmas_produced_c(u), d_skolemized(u), + d_ierCounter_c(c), //d_ierCounter(c), //d_ierCounter_lc(c), //d_ierCounterLastLc(c), @@ -143,6 +144,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_total_inst_count_debug = 0; //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; + d_ierCounter_c = d_ierCounter; d_ierCounter_lc = 0; d_ierCounterLastLc = 0; d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() ); @@ -375,6 +377,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( needsCheck ){ if( Trace.isOn("quant-engine-debug") ){ Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl; + Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl; Trace("quant-engine-debug") << " modules to check : "; for( unsigned i=0; iidentify() << " "; @@ -470,6 +473,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){ d_ierCounter = d_ierCounter + 1; d_ierCounterLastLc = d_ierCounter_lc; + d_ierCounter_c = d_ierCounter_c.get() + 1; } }else if( e==Theory::EFFORT_LAST_CALL ){ d_ierCounter_lc = d_ierCounter_lc + 1; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 228ac9ee9..920c45c1a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -204,6 +204,7 @@ private: std::map< Node, int > d_temp_inst_debug; int d_total_inst_count_debug; /** inst round counters TODO: make context-dependent? */ + context::CDO< int > d_ierCounter_c; int d_ierCounter; int d_ierCounter_lc; int d_ierCounterLastLc; diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index bcf6403b7..4bc16ea25 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -44,7 +44,8 @@ BUG_TESTS = \ bug-fmf-fun-skolem.smt2 \ bug674.smt2 \ inc-double-u.smt2 \ - fmf-fun-dbu.smt2 + fmf-fun-dbu.smt2 \ + inc-define.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/inc-define.smt2 b/test/regress/regress0/push-pop/inc-define.smt2 new file mode 100644 index 000000000..27261eff6 --- /dev/null +++ b/test/regress/regress0/push-pop/inc-define.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic QF_LIA) +(declare-fun x () Int) +(check-sat) +(define t (not (= x 0))) +(assert t) +(check-sat)