From: Andrew Reynolds Date: Tue, 4 Sep 2018 19:34:21 +0000 (-0500) Subject: Make quantifiers strategies exit immediately when in conflict (#2099) X-Git-Tag: cvc5-1.0.0~4688 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d367c9f9b299a15fb970d62df04d3df22b7ca08d;p=cvc5.git Make quantifiers strategies exit immediately when in conflict (#2099) --- diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index eb3f6232d..78fb987f1 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -426,6 +426,7 @@ int InstMatchGenerator::getNextMatch(Node f, Node t = d_curr_first_candidate; do{ Trace("matching-debug2") << "Matching candidate : " << t << std::endl; + Assert(!qe->inConflict()); //if t not null, try to fit it into match m if( !t.isNull() ){ if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){ @@ -439,7 +440,7 @@ int InstMatchGenerator::getNextMatch(Node f, } //get the next candidate term t if( success<0 ){ - t = d_cg->getNextCandidate(); + t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate(); }else{ d_curr_first_candidate = d_cg->getNextCandidate(); } @@ -1029,10 +1030,11 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, if( d_pol ){ tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op ); }else{ - Node r = qe->getEqualityQuery()->getRepresentative( d_eqc ); //iterate over all classes except r tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op ); - if( tat ){ + if (tat && !qe->inConflict()) + { + Node r = qe->getEqualityQuery()->getRepresentative(d_eqc); for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ if( it->first!=r ){ InstMatch m( q ); @@ -1042,12 +1044,13 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, } } } - tat = NULL; } + tat = nullptr; } } Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; - if( tat ){ + if (tat && !qe->inConflict()) + { InstMatch m( q ); addInstantiations( m, qe, addedLemmas, 0, tat ); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 02c9aedf5..92a355348 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -268,7 +268,10 @@ bool QuantInfo::reset_round( QuantConflictFind * p ) { d_mg->reset_round( p ); for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){ - it->second->reset_round( p ); + if (!it->second->reset_round(p)) + { + return false; + } } //now, reset for matching d_mg->reset( p, false, this ); @@ -1178,11 +1181,14 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars } } - -void MatchGen::reset_round( QuantConflictFind * p ) { +bool MatchGen::reset_round(QuantConflictFind* p) +{ d_wasSet = false; for( unsigned i=0; i::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){ d_qni_gterm_rep[it->first] = p->getRepresentative( it->second ); @@ -1194,18 +1200,31 @@ void MatchGen::reset_round( QuantConflictFind * p ) { //}else if( e==-1 ){ // d_ground_eval[0] = p->d_false; //} - //modified - for( unsigned i=0; i<2; i++ ){ - if( p->getTermDatabase()->isEntailed( d_n, i==0 ) ){ + //modified + TermDb* tdb = p->getTermDatabase(); + QuantifiersEngine* qe = p->getQuantifiersEngine(); + for( unsigned i=0; i<2; i++ ){ + if (tdb->isEntailed(d_n, i == 0)) + { d_ground_eval[0] = i==0 ? p->d_true : p->d_false; } + if (qe->inConflict()) + { + return false; + } } }else if( d_type==typ_eq ){ - for (unsigned i = 0; i < d_n.getNumChildren(); i++) + TermDb* tdb = p->getTermDatabase(); + QuantifiersEngine* qe = p->getQuantifiersEngine(); + for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++) { if (!expr::hasBoundVar(d_n[i])) { - TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]); + TNode t = tdb->getEntailedTerm(d_n[i]); + if (qe->inConflict()) + { + return false; + } if (t.isNull()) { d_ground_eval[i] = d_n[i]; @@ -1220,6 +1239,7 @@ void MatchGen::reset_round( QuantConflictFind * p ) { d_qni_bound_cons.clear(); d_qni_bound_cons_var.clear(); d_qni_bound.clear(); + return true; } void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { @@ -2038,9 +2058,10 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) } } Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; - if( d_conflict || d_quantEngine->inConflict() ){ - break; - } + } + if (d_conflict || d_quantEngine->inConflict()) + { + break; } } } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index d76495b52..0469e958b 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -90,7 +90,13 @@ public: std::vector< MatchGen > d_children; short d_type; bool d_type_not; - void reset_round( QuantConflictFind * p ); + /** reset round + * + * Called once at the beginning of each full/last-call effort, prior to + * processing this match generator. This method returns false if the reset + * failed, e.g. if a conflict was encountered during term indexing. + */ + bool reset_round(QuantConflictFind* p); void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ); bool getNextMatch( QuantConflictFind * p, QuantInfo * qi ); bool isValid() { return d_type!=typ_invalid; } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 63593c662..ca9b88ecf 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -621,6 +621,7 @@ REG0_TESTS = \ regress0/quantifiers/issue1805.smt2 \ regress0/quantifiers/issue2031-bv-var-elim.smt2 \ regress0/quantifiers/issue2033-macro-arith.smt2 \ + regress0/quantifiers/issue2035.smt2 \ regress0/quantifiers/lra-triv-gn.smt2 \ regress0/quantifiers/macros-int-real.smt2 \ regress0/quantifiers/macros-real-arg.smt2 \ diff --git a/test/regress/regress0/quantifiers/issue2035.smt2 b/test/regress/regress0/quantifiers/issue2035.smt2 new file mode 100644 index 000000000..4c677d352 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue2035.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --inst-when=full --full-saturate-quant +; EXPECT: unsat +(set-logic AUFLIA) +(set-info :status unsat) +(declare-fun _substvar_37_ () Int) +(declare-fun _substvar_33_ () Int) +(declare-fun _substvar_32_ () Int) +(declare-sort A 0) +(declare-sort PZA 0) +(declare-fun MS (Int A PZA) Bool) +(declare-fun length (PZA Int) Bool) +(declare-fun p () PZA) +(assert (! (exists ((n55 Int)) (and true true (forall ((x862 Int) (x863 A) (x864 A)) (=> (and (MS x862 x863 p) (MS x862 x864 p)) (= x863 x864))) true)) :named hyp30)) +(assert (! (exists ((x1298 A) (x1299 A) (x1300 Int)) (exists ((x1302 Int)) (length p 0))) :named hyp42)) +(assert (! (not (exists ((n67 Int)) (and true true (forall ((x1308 Int) (x1309 A) (x1310 A)) (=> (and (exists ((i114 Int)) (and true true (= _substvar_32_ _substvar_33_) (exists ((x1312 Int)) (and (forall ((x1313 Int)) (=> (length p 0) (= x1312 (+ (- 0 _substvar_33_) 1)))) (MS x1312 x1309 p))))) (exists ((i115 Int)) (and true true (= _substvar_32_ _substvar_37_) (exists ((x1315 Int)) (and (forall ((x1316 Int)) (=> (length p 0) (= x1315 (+ (- 0 _substvar_37_) 1)))) (MS x1315 x1310 p)))))) (= x1309 x1310))) true))) :named goal)) +(check-sat)