From bab37658aa27ee455e3928c66db49c1bb3224e3b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 24 Feb 2016 12:19:09 -0600 Subject: [PATCH] Add entailment checks between length terms to reduce splitting in strings solver. Minor additions to datatypes and qcf. --- src/options/strings_options | 2 + src/theory/datatypes/theory_datatypes.cpp | 51 ++++++++++++++++++- src/theory/datatypes/theory_datatypes.h | 3 ++ .../quantifiers/quant_conflict_find.cpp | 20 +++++++- src/theory/strings/theory_strings.cpp | 21 +++++++- src/theory/uf/theory_uf_strong_solver.cpp | 2 +- 6 files changed, 93 insertions(+), 6 deletions(-) diff --git a/src/options/strings_options b/src/options/strings_options index 65c293dbc..1b64af83f 100644 --- a/src/options/strings_options +++ b/src/options/strings_options @@ -53,6 +53,8 @@ option stringInferSym strings-infer-sym --strings-infer-sym bool :default true strings split on empty string option stringEagerLen strings-eager-len --strings-eager-len bool :default true strings eager length lemmas +option stringCheckEntailLen strings-check-entail-len --strings-check-entail-len bool :default true + check entailment between length terms to reduce splitting endmodule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 51300bfba..3659350b5 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -233,9 +233,11 @@ void TheoryDatatypes::check(Effort e) { //all other cases std::vector< bool > pcons; getPossibleCons( eqc, n, pcons ); + //std::map< int, bool > sel_apps; + //getSelectorsForCons( n, sel_apps ); //check if we do not need to resolve the constructor type for this equivalence class. - // this is if there are no selectors for this equivalence class, its possible values are infinite, - // and we are not producing a model, then do not split. + // this is if there are no selectors for this equivalence class, and its possible values are infinite, + // then do not split. int consIndex = -1; int fconsIndex = -1; bool needSplit = true; @@ -959,6 +961,17 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > } } +void TheoryDatatypes::getSelectorsForCons( Node r, std::map< int, bool >& sels ) { + NodeListMap::iterator sel_i = d_selector_apps.find( r ); + if( sel_i != d_selector_apps.end() ){ + NodeList* sel = (*sel_i).second; + for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){ + int sindex = Datatype::indexOf( (*j).getOperator().toExpr() ); + sels[sindex] = true; + } + } +} + void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) { if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){ std::stringstream ss; @@ -2095,6 +2108,40 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& return false; } +std::pair TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) { + Trace("dt-entail") << "Check entailed : " << lit << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + if( atom.getKind()==APPLY_TESTER ){ + Node n = atom[0]; + if( hasTerm( n ) ){ + Node r = d_equalityEngine.getRepresentative( n ); + EqcInfo * ei = getOrMakeEqcInfo( r, false ); + int l_index = getLabelIndex( ei, r ); + int t_index = (int)Datatype::indexOf( atom.getOperator().toExpr() ); + Trace("dt-entail") << " Tester indices are " << t_index << " and " << l_index << std::endl; + if( l_index!=-1 && (l_index==t_index)==pol ){ + std::vector< TNode > exp_c; + if( ei && !ei->d_constructor.get().isNull() ){ + explainEquality( n, ei->d_constructor.get(), true, exp_c ); + }else{ + Node lbl = getLabel( n ); + Assert( !lbl.isNull() ); + exp_c.push_back( lbl ); + Assert( areEqual( n, lbl[0] ) ); + explainEquality( n, lbl[0], true, exp_c ); + } + Node exp = mkAnd( exp_c ); + Trace("dt-entail") << " entailed, explanation is " << exp << std::endl; + return make_pair(true, exp); + } + } + }else{ + + } + return make_pair(false, Node::null()); +} + } /* namepsace CVC4::theory::datatypes */ } /* namepsace CVC4::theory */ } /* namepsace CVC4 */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index d56538b2a..2f6c6e6bb 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -131,6 +131,7 @@ private: bool hasTester( Node n ); /** get the possible constructors for n */ void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons ); + void getSelectorsForCons( Node r, std::map< int, bool >& sels ); /** mkExpDefSkolem */ void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ); /** skolems for terms */ @@ -260,6 +261,8 @@ public: std::string identify() const { return std::string("TheoryDatatypes"); } /** debug print */ void printModelDebug( const char* c ); + /** entailment check */ + virtual std::pair entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); private: /** add tester to equivalence class info */ void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg ); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 5cff55d21..779c0c44e 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -477,7 +477,22 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl; return false; }else if( rew!=p->d_true ){ - //if checking for conflicts, we must be sure that the constraint is entailed + //if checking for conflicts, we must be sure that the (negation of) constraint is (not) entailed + if( !chEnt ){ + rew = Rewriter::rewrite( rew.negate() ); + } + //check if it is entailed + Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl; + std::pair et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew ); + ++(p->d_statistics.d_entailment_checks); + Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl; + if( !et.first ){ + Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl; + return !chEnt; + }else{ + return chEnt; + } +/* if( chEnt ){ //check if it is entailed Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl; @@ -494,6 +509,7 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl; return true; } +*/ }else{ Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl; return true; @@ -1681,6 +1697,8 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { bool MatchGen::isHandledUfTerm( TNode n ) { //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT || // n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; + //TODO : treat APPLY_TESTER as a T-constraint instead of matching (currently leads to overabundance of instantiations) + //return inst::Trigger::isAtomicTriggerKind( n.getKind() ) && ( !options::qcfTConstraint() || n.getKind()!=APPLY_TESTER ); return inst::Trigger::isAtomicTriggerKind( n.getKind() ); } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 529e69e82..a4ebe5e97 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2012,11 +2012,28 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form antec_new_lits.push_back( xgtz ); } } - Node sk = mkSkolemCached( normal_forms[i][index_i], normal_forms[j][index_j], sk_id_v_spt, "v_spt", 1 ); Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) ); Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) ); - conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 )); + if( options::stringCheckEntailLen() ){ + //check entailment + for( unsigned e=0; e<2; e++ ){ + Node lt1 = e==0 ? length_term_i : length_term_j; + Node lt2 = e==0 ? length_term_j : length_term_i; + Node ent_lit = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, lt1, lt2 ) ); + std::pair et = d_valuation.entailmentCheck(THEORY_OF_TYPE_BASED, ent_lit ); + if( et.first ){ + Trace("strings-entail") << "Strings entailment : " << ent_lit << " is entailed in the current context." << std::endl; + Trace("strings-entail") << " explanation was : " << et.second << std::endl; + conc = e==0 ? eq1 : eq2; + antec_new_lits.push_back( et.second ); + } + } + } + if( conc.isNull() ){ + conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 )); + } + Node ant = mkExplain( antec, antec_new_lits ); sendLemma( ant, conc, "S-Split(VAR)" ); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 3ed1c4d40..661c67354 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1346,7 +1346,7 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){ eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) ); } - Node ax = NodeManager::currentNM()->mkNode( OR, eqs ); + Node ax = eqs.size()==1 ? eqs[0] : NodeManager::currentNM()->mkNode( OR, eqs ); Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax ); Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl; d_thss->getOutputChannel().lemma( lem ); -- 2.30.2