From c87ee73ad3d51c238700f236c18e425b80e8e7ac Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 5 May 2016 18:44:47 -0500 Subject: [PATCH] Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs. --- proofs/lfsc_checker/check.cpp | 2 +- proofs/lfsc_checker/expr.cpp | 2 +- proofs/lfsc_checker/expr.h | 45 ++++- proofs/lfsc_checker/main.cpp | 1 + proofs/signatures/th_bv_bitblast.plf | 38 +++- src/options/options_handler.cpp | 34 ++-- src/options/quantifiers_modes.cpp | 11 +- src/options/quantifiers_modes.h | 10 +- src/options/quantifiers_options | 2 +- src/parser/smt2/Smt2.g | 13 +- src/parser/smt2/smt2.cpp | 2 + .../quantifiers/conjecture_generator.cpp | 9 +- src/theory/quantifiers/inst_propagator.cpp | 90 ++++++--- src/theory/quantifiers/inst_propagator.h | 10 +- .../quantifiers/inst_strategy_e_matching.cpp | 19 +- .../quantifiers/quant_conflict_find.cpp | 187 ++++++++++-------- src/theory/quantifiers/quant_conflict_find.h | 9 +- .../quantifiers/quantifiers_rewriter.cpp | 6 +- src/theory/quantifiers/term_database.cpp | 171 +++++++++------- src/theory/quantifiers/term_database.h | 4 +- src/theory/quantifiers_engine.cpp | 32 ++- src/theory/quantifiers_engine.h | 1 + test/regress/regress0/sygus/Makefile.am | 3 +- test/regress/regress0/sygus/strings-small.sy | 35 ++++ 24 files changed, 491 insertions(+), 245 deletions(-) create mode 100644 test/regress/regress0/sygus/strings-small.sy diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp index c96791aeb..22e326cda 100644 --- a/proofs/lfsc_checker/check.cpp +++ b/proofs/lfsc_checker/check.cpp @@ -24,7 +24,7 @@ int colnum = 1; const char *filename = 0; FILE *curfile = 0; -//#define USE_HASH_MAPS +//#define USE_HASH_MAPS //AJR: deprecated symmap2 progs; std::vector< Expr* > ascHoles; diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp index ae0e49531..5cb774fbf 100644 --- a/proofs/lfsc_checker/expr.cpp +++ b/proofs/lfsc_checker/expr.cpp @@ -34,7 +34,6 @@ bool destroy_progs = false; Expr *r = rr; \ int ref = r->data >> 9; \ ref = ref - 1; \ - r->debugrefcnt(ref,DEC); \ if (ref == 0) { \ _e = r; \ goto start_destroy; \ @@ -43,6 +42,7 @@ bool destroy_progs = false; r->data = (ref << 9) | (r->data & 511); \ } while(0) +//removed from below "ref = ref -1;": r->debugrefcnt(ref,DEC); void Expr::destroy(Expr *_e, bool dec_kids) { start_destroy: diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h index 32a62ab33..5a505a3d9 100644 --- a/proofs/lfsc_checker/expr.h +++ b/proofs/lfsc_checker/expr.h @@ -8,9 +8,9 @@ #include #include "chunking_memory_management.h" -#define USE_FLAT_APP +#define USE_FLAT_APP //AJR: off deprecated #define MARKVAR_32 -#define DEBUG_SYM_NAMES +//#define DEBUG_SYM_NAMES //#define DEBUG_SYMS // Expr class @@ -66,7 +66,6 @@ protected: enum { INC, DEC, CREATE }; void debugrefcnt(int ref, int what) { -#ifdef DEBUG_REFCNT std::cout << "["; debug(); switch(what) { @@ -83,10 +82,6 @@ protected: char tmp[10]; sprintf(tmp,"%d",ref); std::cout << tmp << "]\n"; -#else - (void)ref; - (void)what; -#endif } Expr(int _class, int _op) @@ -114,14 +109,18 @@ public: // std::cout << " " << ref << std::endl; //} ref = ref<4194303 ? ref + 1 : ref; +#ifdef DEBUG_REFCNT debugrefcnt(ref,INC); +#endif data = (ref << 9) | (data & 511); } static void destroy(Expr *, bool); inline void dec(bool dec_kids = true) { int ref = getrefcnt(); ref = ref - 1; +#ifdef DEBUG_REFCNT debugrefcnt(ref,DEC); +#endif if (ref == 0) destroy(this,dec_kids); else @@ -131,10 +130,10 @@ public: //must pass statType (the expr representing "type") to this function bool isType( Expr* statType ); - inline bool isDatatype() { + inline bool isDatatype() const { return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ; } - inline bool isArithTerm() { + inline bool isArithTerm() const { return getop() == ADD || getop() == NEG; } @@ -188,13 +187,17 @@ public: CExpr(int _op) : Expr(CEXPR, _op), kids() { kids = new Expr *[1]; kids[0] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() { kids = new Expr *[2]; kids[0] = e1; kids[1] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, Expr *e1, Expr *e2) : Expr(CEXPR, _op), kids() { @@ -202,7 +205,9 @@ public: kids[0] = e1; kids[1] = e2; kids[2] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, Expr *e1, Expr *e2, Expr *e3) : Expr(CEXPR, _op), kids() { @@ -211,7 +216,9 @@ public: kids[1] = e2; kids[2] = e3; kids[3] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, Expr *e1, Expr *e2, Expr *e3, Expr *e4) : Expr(CEXPR, _op), kids() { @@ -221,7 +228,9 @@ public: kids[2] = e3; kids[3] = e4; kids[4] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, const std::vector &_kids) : Expr(CEXPR, _op), kids() { @@ -230,13 +239,17 @@ public: for (i = 0; i < iend; i++) kids[i] = _kids[i]; kids[i] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } // _kids must be null-terminated. CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) { (void)dummy; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } Expr *whr(); @@ -253,7 +266,9 @@ class IntExpr : public Expr { } IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() { mpz_init_set(n,_n); +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } IntExpr(signed long int _n ) : Expr(INT_EXPR, 0), n() { mpz_init_set_si( n, _n ); @@ -271,7 +286,9 @@ class RatExpr : public Expr { RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() { mpq_init( n ); mpq_set(n,_n); +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif mpq_canonicalize( n ); } RatExpr(signed long int _n1, unsigned long int _n2 ) : Expr(RAT_EXPR, 0), n() { @@ -290,15 +307,19 @@ class SymExpr : public Expr { : Expr(theclass, 0), val(0) { (void)_s; +#ifdef DEBUG_REFCNT if (theclass == SYM_EXPR) debugrefcnt(1,CREATE); +#endif } SymExpr(const SymExpr &e, int theclass = SYM_EXPR) : Expr(theclass, 0), val(0) { (void)e; +#ifdef DEBUG_REFCNT if (theclass == SYM_EXPR) debugrefcnt(1,CREATE); +#endif } #ifdef MARKVAR_32 private: @@ -317,12 +338,16 @@ class SymSExpr : public SymExpr { SymSExpr(std::string _s, int theclass = SYMS_EXPR) : SymExpr(_s, theclass), s(_s) { +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR) : SymExpr(e, theclass), s(e.s) { +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } }; @@ -338,7 +363,9 @@ public: #ifdef DEBUG_HOLE_NAMES id = next_id++; #endif +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } Expr *val; // may be set during subst(), defeq(), and clone(). }; diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp index 80f36e69f..1d8ba5809 100644 --- a/proofs/lfsc_checker/main.cpp +++ b/proofs/lfsc_checker/main.cpp @@ -133,6 +133,7 @@ int main(int argc, char **argv) { a.files.clear(); #endif + std::cout << "Proof checked successfully!" << std::endl << std::endl; std::cout << "time = " << (int)clock() - check_time << std::endl; std::cout << "sym count = " << SymExpr::symmCount << std::endl; std::cout << "marked count = " << Expr::markedCount << std::endl; diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 8e8c51857..580b54418 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -280,7 +280,34 @@ (bbltn (fail bblt)) ((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry)) (bblast_bvadd a' b' carry))))))) - + + +(program reverse_help ((x bblt) (acc bblt)) bblt +(match x + (bbltn acc) + ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) + + +(program reverseb ((x bblt)) bblt + (reverse_help x bbltn)) + + +; AJR: use this version? +;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt +;(match a +; ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) +; ((bbltc ai a') (match b +; (bbltn (fail bblt)) +; ((bbltc bi b') +; (let carry' (or (and ai bi) (and (xor ai bi) carry)) +; (bbltc (xor (xor ai bi) carry) +; (bblast_bvadd_2h a' b' carry')))))))) + +;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt +;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +;(let br (reverseb b) ;; from the least significant bit up +;(let ret (bblast_bvadd_2h ar br carry) +; (reverseb ret))))) (declare bv_bbl_bvadd (! n mpz (! x (term (BitVec n)) @@ -322,15 +349,6 @@ ;; shift add multiplier -(program reverse_help ((x bblt) (acc bblt)) bblt -(match x - (bbltn acc) - ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) - - -(program reverseb ((x bblt)) bblt - (reverse_help x bbltn)) - ;; (program concat ((a bblt) (b bblt)) bblt ;; (match a (bbltn b) ;; ((bbltc ai a') (bbltc ai (concat a' b))))) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index a2809bd67..7d41ae862 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -254,15 +254,21 @@ last-call\n\ const std::string OptionsHandler::s_literalMatchHelp = "\ Literal match modes currently supported by the --literal-match option:\n\ \n\ -none (default)\n\ +none \n\ + Do not use literal matching.\n\ \n\ -predicate\n\ -+ Consider the phase requirements of predicate literals when applying heuristic\n\ - quantifier instantiation. For example, the trigger P( x ) in the quantified \n\ - formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\ - terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\ - Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ +use (default)\n\ ++ Consider phase requirements of triggers conservatively. For example, the\n\ + trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n\ + terms in the equivalence class of true, and likewise Q( x ) will not be matched\n\ + terms in the equivalence class of false. Extends to equality.\n\ +\n\ +agg-predicate \n\ ++ Consider phase requirements aggressively for predicates. In the above example,\n\ + only match P( x ) with terms that are in the equivalence class of false.\n\ +\n\ +agg \n\ ++ Consider the phase requirements aggressively for all triggers.\n\ \n\ "; @@ -506,10 +512,12 @@ void OptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers:: theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) { if(optarg == "none") { return theory::quantifiers::LITERAL_MATCH_NONE; - } else if(optarg == "predicate") { - return theory::quantifiers::LITERAL_MATCH_PREDICATE; - } else if(optarg == "equality") { - return theory::quantifiers::LITERAL_MATCH_EQUALITY; + } else if(optarg == "use") { + return theory::quantifiers::LITERAL_MATCH_USE; + } else if(optarg == "agg-predicate") { + return theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE; + } else if(optarg == "agg") { + return theory::quantifiers::LITERAL_MATCH_AGG; } else if(optarg == "help") { puts(s_literalMatchHelp.c_str()); exit(1); @@ -520,9 +528,7 @@ theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(s } void OptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) { - if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) { - throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release."); - } + } theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) { diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp index a58120974..e2cd78de5 100644 --- a/src/options/quantifiers_modes.cpp +++ b/src/options/quantifiers_modes.cpp @@ -46,11 +46,14 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod case theory::quantifiers::LITERAL_MATCH_NONE: out << "LITERAL_MATCH_NONE"; break; - case theory::quantifiers::LITERAL_MATCH_PREDICATE: - out << "LITERAL_MATCH_PREDICATE"; + case theory::quantifiers::LITERAL_MATCH_USE: + out << "LITERAL_MATCH_USE"; break; - case theory::quantifiers::LITERAL_MATCH_EQUALITY: - out << "LITERAL_MATCH_EQUALITY"; + case theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE: + out << "LITERAL_MATCH_AGG_PREDICATE"; + break; + case theory::quantifiers::LITERAL_MATCH_AGG: + out << "LITERAL_MATCH_AGG"; break; default: out << "LiteralMatchMode!UNKNOWN"; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 5749da972..b4b9abdaf 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -44,10 +44,12 @@ enum InstWhenMode { enum LiteralMatchMode { /** Do not consider polarity of patterns */ LITERAL_MATCH_NONE, - /** Consider polarity of boolean predicates only */ - LITERAL_MATCH_PREDICATE, - /** Consider polarity of boolean predicates, as well as equalities */ - LITERAL_MATCH_EQUALITY, + /** Conservatively consider polarity of patterns */ + LITERAL_MATCH_USE, + /** Aggressively consider polarity of Boolean predicates */ + LITERAL_MATCH_AGG_PREDICATE, + /** Aggressively consider polarity of all terms */ + LITERAL_MATCH_AGG, }; enum MbqiMode { diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index f69a8df8b..9fef0295e 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -120,7 +120,7 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true option fullSaturateInst --fs-inst bool :default false interleave full saturate instantiation with other techniques -option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode +option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_USE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode choose literal matching mode ### finite model finding options diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 38163c579..c28d23eac 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -760,7 +760,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL] body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body); Debug("parser-sygus") << "...constructed exists " << body << std::endl; } - body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr); + if( !PARSER_STATE->getSygusFunSymbols().empty() ){ + body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr); + } Debug("parser-sygus") << "...constructed forall " << body << std::endl; Command* c = new SetUserAttributeCommand("sygus", sygusVar); c->setMuted(true); @@ -791,6 +793,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] std::string sname; std::vector< Expr > let_vars; bool readingLet = false; + std::string s; } : LPAREN_TOK //read operator @@ -890,6 +893,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL); sgt.d_gterm_type = SygusGTerm::gterm_op; } + | str[s,false] + { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl; + sgt.d_expr = MK_CONST( ::CVC4::String(s) ); + sgt.d_name = s; + sgt.d_gterm_type = SygusGTerm::gterm_op; + } | symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )? { if( readEnum ){ name = name + "__Enum__" + name2; @@ -2773,7 +2782,7 @@ STRING_LITERAL_2_0 * will be part of the token text. Use the str[] parser rule instead. */ STRING_LITERAL_2_5 - : { PARSER_STATE->v2_5() }?=> + : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=> '"' (~('"') | '""')* '"' ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ebad90583..2da44152a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -350,6 +350,8 @@ void Smt2::setLogic(std::string name) { name = "UFLIRA"; } else if(name == "BV") { name = "UFBV"; + } else if(name == "SLIA") { + name = "UFSLIA"; } else if(name == "ALL_SUPPORTED") { //no change } else { diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index fa71f0132..f4eb67d74 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1572,7 +1572,6 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, if( d_match_status_child_num==0 ){ //initial binding TNode f = s->getTgFunc( d_typ, d_status_num ); - //std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc ); Assert( !eqc.isNull() ); TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f ); if( tat ){ @@ -1726,9 +1725,9 @@ void TermGenEnv::collectSignatureInformation() { d_func_kind.clear(); d_func_args.clear(); TypeNode tnull; - for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){ - if( getTermDatabase()->getNumGroundTerms( it->first )>0 ){ - Node nn = getTermDatabase()->getGroundTerm( it->first, 0 ); + for( std::map< Node, std::vector< Node > >::iterator it = getTermDatabase()->d_op_map.begin(); it != getTermDatabase()->d_op_map.end(); ++it ){ + if( !it->second.empty() ){ + Node nn = it->second[0]; Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl; if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){ bool do_enum = true; @@ -1750,7 +1749,7 @@ void TermGenEnv::collectSignatureInformation() { d_typ_tg_funcs[nn.getType()].push_back( it->first ); d_tg_func_param[it->first] = ( nn.getMetaKind() == kind::metakind::PARAMETERIZED ); Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl; - getTermDatabase()->computeUfEqcTerms( it->first ); + //getTermDatabase()->computeUfEqcTerms( it->first ); } } Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl; diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 1dc6f6d50..41c9c40c8 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -34,6 +34,7 @@ bool EqualityQueryInstProp::reset( Theory::Effort e ) { d_uf.clear(); d_uf_exp.clear(); d_diseq_list.clear(); + d_uf_func_map_trie.clear(); return true; } @@ -103,7 +104,7 @@ TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& arg if( !t.isNull() ){ return t; }else{ - return d_func_map_trie[f].existsTerm( args ); + return d_uf_func_map_trie[f].existsTerm( args ); } } @@ -168,6 +169,21 @@ bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& } } +TNode EqualityQueryInstProp::getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ) { + TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args ); + if( !t.isNull() ){ + return t; + }else{ + TNode tt = d_uf_func_map_trie[f].existsTerm( args ); + if( !tt.isNull() ){ + //TODO? + return tt; + }else{ + return tt; + } + } +} + Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) { Assert( exp.empty() ); std::map< Node, Node >::iterator it = d_uf.find( a ); @@ -279,11 +295,13 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No Assert( d_uf_exp[ar].empty() ); Assert( d_uf_exp[br].empty() ); + //registerUfTerm( ar ); d_uf[ar] = br; merge_exp( d_uf_exp[ar], exp_a ); merge_exp( d_uf_exp[ar], exp_b ); merge_exp( d_uf_exp[ar], reason ); + //registerUfTerm( br ); d_uf[br] = br; d_uf_exp[br].clear(); @@ -316,6 +334,25 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No } } +void EqualityQueryInstProp::registerUfTerm( TNode n ) { + if( d_uf.find( n )==d_uf.end() ){ + if( !getEngine()->hasTerm( n ) ){ + TNode f = d_qe->getTermDatabase()->getMatchOperator( n ); + if( !f.isNull() ){ + std::vector< TNode > args; + for( unsigned i=0; ihasTerm( n[i] ) ){ + return; + }else{ + args.push_back( n[i] ); + } + } + d_uf_func_map_trie[f].addTerm( n, args ); + } + } + } +} + //void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) { void EqualityQueryInstProp::addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ) { if( is_watch ){ @@ -573,6 +610,7 @@ bool InstPropagator::reset( Theory::Effort e ) { d_watch_list.clear(); d_update_list.clear(); d_relevant_inst.clear(); + d_has_relevant_inst = false; return d_qy.reset( e ); } @@ -607,7 +645,31 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st return !d_conflict; }else{ Assert( false ); - return true; + return false; + } +} + +void InstPropagator::filterInstantiations() { + if( d_has_relevant_inst ){ + //now, inform quantifiers engine which instances should be retracted + Trace("qip-prop-debug") << "...remove instantiation ids : "; + for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){ + if( !it->second.d_q.isNull() ){ + if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){ + if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){ + Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; + Assert( false ); + }else{ + Trace("qip-prop-debug") << it->first << " "; + } + }else{ + //mark the quantified formula as relevant + d_qe->markRelevant( it->second.d_q ); + } + } + } + Trace("qip-prop-debug") << std::endl; + Trace("quant-engine-conflict") << "-----> InstPropagator::" << ( d_conflict ? "conflict" : "propagate" ) << " with " << d_relevant_inst.size() << " instances." << std::endl; } } @@ -720,10 +782,12 @@ void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& e } if( pol ){ if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){ + Trace("qip-rlv-propagate") << "Relevant propagation : " << a << ( pol ? " == " : " != " ) << b << std::endl; Assert( d_qy.getEngine()->hasTerm( a ) ); Assert( d_qy.getEngine()->hasTerm( b ) ); Trace("qip-prop-debug") << "...equality between known terms." << std::endl; addRelevantInstances( exp, "qip-propagate" ); + //d_has_relevant_inst = true; } Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl; for( unsigned i=0; i<2; i++ ){ @@ -750,27 +814,7 @@ void InstPropagator::conflict( std::vector< Node >& exp ) { d_conflict = true; d_relevant_inst.clear(); addRelevantInstances( exp, "qip-propagate" ); - - //now, inform quantifiers engine which instances should be retracted - Trace("qip-prop-debug") << "...remove instantiation ids : "; - for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){ - if( !it->second.d_q.isNull() ){ - if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){ - if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){ - Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; - Assert( false ); - }else{ - Trace("qip-prop-debug") << it->first << " "; - } - }else{ - //mark the quantified formula as relevant - d_qe->markRelevant( it->second.d_q ); - } - } - } - Trace("qip-prop-debug") << std::endl; - //will interupt the quantifiers engine - Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl; + d_has_relevant_inst = true; } bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) { diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index 61aa8257f..6201cf152 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -64,9 +64,11 @@ public: bool areEqualExp( Node a, Node b, std::vector< Node >& exp ); /** returns true is a and b are disequal in the current context */ bool areDisequalExp( Node a, Node b, std::vector< Node >& exp ); + /** get congruent term */ + TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ); private: /** term index */ - std::map< Node, TermArgTrie > d_func_map_trie; + std::map< Node, TermArgTrie > d_uf_func_map_trie; /** union find for terms beyond what is stored in equality engine */ std::map< Node, Node > d_uf; std::map< Node, std::vector< Node > > d_uf_exp; @@ -75,6 +77,8 @@ private: std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list; /** add arg */ void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ); + /** register term */ + void registerUfTerm( TNode n ); public: enum { STATUS_CONFLICT, @@ -110,10 +114,13 @@ private: virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); } + virtual void filterInstantiations() { d_ip.filterInstantiations(); } }; InstantiationNotifyInstPropagator d_notify; /** notify instantiation method */ bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ); + /** remove instance ids */ + void filterInstantiations(); /** allocate instantiation */ unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ); /** equality query */ @@ -142,6 +149,7 @@ private: std::vector< unsigned > d_update_list; /** relevant instances */ std::map< unsigned, bool > d_relevant_inst; + bool d_has_relevant_inst; private: bool update( unsigned id, InstInfo& i, bool firstTime = false ); void propagate( Node a, Node b, bool pol, std::vector< Node >& exp ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index d58bbcf3a..7bc51dc50 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -332,19 +332,30 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ unsigned num_fv = tinfo[pat].d_fv.size(); Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl; if( rpol!=0 ){ + Assert( rpol==1 || rpol==-1 ); if( Trigger::isRelationalTrigger( pat ) ){ pat = rpol==-1 ? pat.negate() : pat; }else{ Assert( Trigger::isAtomicTrigger( pat ) ); if( pat.getType().isBoolean() && rpoleq.isNull() ){ - pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); + if( options::literalMatchMode()==LITERAL_MATCH_USE ){ + pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); + }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){ + pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==1 ) ); + } }else{ Assert( !rpoleq.isNull() ); if( rpol==-1 ){ - //all equivalence classes except rpoleq - pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate(); + if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){ + //all equivalence classes except rpoleq + pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate(); + } }else if( rpol==1 ){ - //all equivalence classes that are not disequal to rpoleq TODO + if( options::literalMatchMode()==LITERAL_MATCH_AGG ){ + //only equivalence class rpoleq + pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ); + } + //all equivalence classes that are not disequal to rpoleq TODO? } } } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 52563978f..1365feda9 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -119,7 +119,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { //} //get all variables that are always relevant std::map< TNode, bool > visited; - getPropagateVars( vars, q[1], false, visited ); + getPropagateVars( p, vars, q[1], false, visited ); for( unsigned j=0; jgetTermDatabase()->getMatchOperator( v ); @@ -140,7 +140,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { } } -void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){ +void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){ std::map< TNode, bool >::iterator itv = visited.find( n ); if( itv==visited.end() ){ visited[n] = true; @@ -149,6 +149,12 @@ void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, if( d_var_num.find( n )!=d_var_num.end() ){ Assert( std::find( vars.begin(), vars.end(), n )==vars.end() ); vars.push_back( n ); + TNode f = p->getTermDatabase()->getMatchOperator( n ); + if( !f.isNull() ){ + if( std::find( p->d_func_rel_dom[f].begin(), p->d_func_rel_dom[f].end(), d_q )==p->d_func_rel_dom[f].end() ){ + p->d_func_rel_dom[f].push_back( d_q ); + } + } }else if( MatchGen::isHandledBoolConnective( n ) ){ Assert( n.getKind()!=IMPLIES ); QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol ); @@ -156,7 +162,7 @@ void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl; if( rec ){ for( unsigned i=0; i >::iterator it = d_var_constraint[r].begin(); @@ -263,7 +270,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) { d_mg->d_children.clear(); d_mg->d_n = NodeManager::currentNM()->mkConst( true ); d_mg->d_type = MatchGen::typ_ground; - return; + return false; } } } @@ -274,6 +281,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) { } //now, reset for matching d_mg->reset( p, false, this ); + return true; } int QuantInfo::getCurrentRepVar( int v ) { @@ -1283,11 +1291,14 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { } }else if( d_type==typ_var ){ Assert( isHandledUfTerm( d_n ) ); - Node f = getMatchOperator( p, d_n ); + TNode f = getMatchOperator( p, d_n ); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f ); if( qni!=NULL ){ d_qn.push_back( qni ); + }else{ + //inform irrelevant quantifiers + p->setIrrelevantFunction( f ); } d_matched_basis = false; }else if( d_type==typ_tsym || d_type==typ_tconstraint ){ @@ -2013,6 +2024,18 @@ void QuantConflictFind::reset_round( Theory::Effort level ) { d_needs_computeRelEqr = true; } +void QuantConflictFind::setIrrelevantFunction( TNode f ) { + if( d_irr_func.find( f )==d_irr_func.end() ){ + d_irr_func[f] = true; + std::map< TNode, std::vector< Node > >::iterator it = d_func_rel_dom.find( f ); + if( it != d_func_rel_dom.end()){ + for( unsigned j=0; jsecond.size(); j++ ){ + d_irr_quant[it->second[j]] = true; + } + } + } +} + /** check */ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){ @@ -2035,14 +2058,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { } computeRelevantEqr(); - //determine order for quantified formulas - std::vector< Node > qorder; - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); - if( d_quantEngine->hasOwnership( q, this ) ){ - qorder.push_back( q ); - } - } + d_irr_func.clear(); + d_irr_quant.clear(); + if( Trace.isOn("qcf-debug") ){ Trace("qcf-debug") << std::endl; debugPrint("qcf-debug"); @@ -2053,80 +2071,83 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { for( short e = effort_conflict; e<=end_e; e++ ){ d_effort = e; Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl; - for( unsigned j=0; jmatchGeneratorIsValid() ){ - Trace("qcf-check") << "Check quantified formula "; - debugPrintQuant("qcf-check", q); - Trace("qcf-check") << " : " << q << "..." << std::endl; - - Trace("qcf-check-debug") << "Reset round..." << std::endl; - qi->reset_round( this ); - //try to make a matches making the body false - Trace("qcf-check-debug") << "Get next match..." << std::endl; - while( qi->getNextMatch( this ) ){ - Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - if( !qi->isMatchSpurious( this ) ){ - std::vector< int > assigned; - if( qi->completeMatch( this, assigned ) ){ - std::vector< Node > terms; - qi->getMatch( terms ); - bool tcs = qi->isTConstraintSpurious( this, terms ); - if( !tcs ){ - //for debugging - if( Debug.isOn("qcf-check-inst") ){ - Node inst = d_quantEngine->getInstantiation( q, terms ); - Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( !getTermDatabase()->isEntailed( inst, true ) ); - Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); - } - if( d_quantEngine->addInstantiation( q, terms ) ){ - Trace("qcf-check") << " ... Added instantiation" << std::endl; - Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - ++addedLemmas; - if( e==effort_conflict ){ - d_quantEngine->markRelevant( q ); - ++(d_statistics.d_conflict_inst); - if( options::qcfAllConflict() ){ - isConflict = true; + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); + if( d_quantEngine->hasOwnership( q, this ) && d_irr_quant.find( q )==d_irr_quant.end() ){ + QuantInfo * qi = &d_qinfo[q]; + + Assert( d_qinfo.find( q )!=d_qinfo.end() ); + if( qi->matchGeneratorIsValid() ){ + Trace("qcf-check") << "Check quantified formula "; + debugPrintQuant("qcf-check", q); + Trace("qcf-check") << " : " << q << "..." << std::endl; + + Trace("qcf-check-debug") << "Reset round..." << std::endl; + if( qi->reset_round( this ) ){ + //try to make a matches making the body false + Trace("qcf-check-debug") << "Get next match..." << std::endl; + while( qi->getNextMatch( this ) ){ + Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + if( !qi->isMatchSpurious( this ) ){ + std::vector< int > assigned; + if( qi->completeMatch( this, assigned ) ){ + std::vector< Node > terms; + qi->getMatch( terms ); + bool tcs = qi->isTConstraintSpurious( this, terms ); + if( !tcs ){ + //for debugging + if( Debug.isOn("qcf-check-inst") ){ + Node inst = d_quantEngine->getInstantiation( q, terms ); + Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; + Assert( !getTermDatabase()->isEntailed( inst, true ) ); + Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); + } + if( d_quantEngine->addInstantiation( q, terms ) ){ + Trace("qcf-check") << " ... Added instantiation" << std::endl; + Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + ++addedLemmas; + if( e==effort_conflict ){ + d_quantEngine->markRelevant( q ); + ++(d_statistics.d_conflict_inst); + if( options::qcfAllConflict() ){ + isConflict = true; + }else{ + d_conflict.set( true ); + } + break; + }else if( e==effort_prop_eq ){ + d_quantEngine->markRelevant( q ); + ++(d_statistics.d_prop_inst); + } }else{ - d_conflict.set( true ); + Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; + //this should only happen if the algorithm generates the same propagating instance twice this round + //in this case, break to avoid exponential behavior + break; } - break; - }else if( e==effort_prop_eq ){ - d_quantEngine->markRelevant( q ); - ++(d_statistics.d_prop_inst); + }else{ + Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; } + //clean up assigned + qi->revertMatch( this, assigned ); + d_tempCache.clear(); }else{ - Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; - //this should only happen if the algorithm generates the same propagating instance twice this round - //in this case, break to avoid exponential behavior - break; + Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; } }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; + Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; } - //clean up assigned - qi->revertMatch( this, assigned ); - d_tempCache.clear(); - }else{ - Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; } - }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; + Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; + if( d_conflict ){ + break; + } } } - Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; - if( d_conflict ){ - break; - } } } if( addedLemmas>0 ){ @@ -2157,17 +2178,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { void QuantConflictFind::computeRelevantEqr() { if( d_needs_computeRelEqr ){ d_needs_computeRelEqr = false; - Trace("qcf-check") << "Compute relevant equalities..." << std::endl; - //d_uf_terms.clear(); - //d_eqc_uf_terms.clear(); + Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl; d_eqcs.clear(); - //d_arg_reps.clear(); - //double clSet = 0; - //if( Trace.isOn("qcf-opt") ){ - // clSet = double(clock())/double(CLOCKS_PER_SEC); - //} - //now, store matches eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); while( !eqcs_i.isFinished() ){ Node r = (*eqcs_i); diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 16f6b6a1b..974495269 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -117,7 +117,7 @@ private: //for completing match std::vector< int > d_una_eqc_count; //optimization: track which arguments variables appear under UF terms in std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom; - void getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ); + void getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ); //optimization: number of variables set, to track when we can stop std::map< int, bool > d_vars_set; std::map< Node, bool > d_ground_terms; @@ -156,7 +156,7 @@ public: } Node d_q; - void reset_round( QuantConflictFind * p ); + bool reset_round( QuantConflictFind * p ); public: //initialize void initialize( QuantConflictFind * p, Node q, Node qn ); @@ -195,6 +195,11 @@ private: std::map< Kind, Node > d_zero; //for storing nodes created during t-constraint solving (prevents memory leaks) std::vector< Node > d_tempCache; + //optimization: list of quantifiers that depend on ground function applications + std::map< TNode, std::vector< Node > > d_func_rel_dom; + std::map< TNode, bool > d_irr_func; + std::map< Node, bool > d_irr_quant; + void setIrrelevantFunction( TNode f ); private: std::map< Node, Node > d_op_node; int d_fid_count; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 2f7864831..6963f7e62 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -187,7 +187,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { std::vector< Node > args; Node body = in; bool doRewrite = false; - bool firstTime = true; while( body.getNumChildren()==2 && body.getKind()==body[1].getKind() ){ for( unsigned i=0; i children; + for( unsigned i=0; imkNode(kind::BOUND_VAR_LIST,args) ); - children.push_back( body ); + children.push_back( body[1] ); Node n = NodeManager::currentNM()->mkNode( in.getKind(), children ); if( in!=n ){ Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index b143286cc..61c02d3ac 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -163,6 +163,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi //if this is an atomic trigger, consider adding it if( inst::Trigger::isAtomicTrigger( n ) ){ Trace("term-db") << "register term in db " << n << std::endl; + if( options::finiteModelFind() ){ + computeModelBasisArgAttribute( n ); + } + Node op = getMatchOperator( n ); d_op_map[op].push_back( n ); added.insert( n ); @@ -222,7 +226,86 @@ void TermDb::computeUfEqcTerms( TNode f ) { } } +void TermDb::computeUfTerms( TNode f ) { + if( d_op_nonred_count.find( f )==d_op_nonred_count.end() ){ + d_op_nonred_count[ f ] = 0; + std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); + if( it!=d_op_map.end() ){ + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + Trace("term-db-debug") << "Adding terms for operator " << f << std::endl; + for( unsigned i=0; isecond.size(); i++ ){ + Node n = it->second[i]; + //to be added to term index, term must be relevant, and exist in EE + if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ + if( isTermActive( n ) ){ + computeArgReps( n ); + + Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; + for( unsigned i=0; igetRepresentative( n ) << std::endl; + Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] ); + Trace("term-db-debug2") << "...add term returned " << at << std::endl; + if( at!=n && ee->areEqual( at, n ) ){ + setTermInactive( n ); + Trace("term-db-debug") << n << " is redundant." << std::endl; + //congruentCount++; + }else{ + if( at!=n && ee->areDisequal( at, n, false ) ){ + std::vector< Node > lits; + lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) ); + for( unsigned i=0; imkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() ); + } + } + Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); + if( Trace.isOn("term-db-lemma") ){ + Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; + if( !d_quantEngine->getTheoryEngine()->needCheck() ){ + Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; + } + Trace("term-db-lemma") << " add lemma : " << lem << std::endl; + } + d_quantEngine->addLemma( lem ); + d_consistent_ee = false; + return; + } + //nonCongruentCount++; + d_op_nonred_count[ f ]++; + } + }else{ + Trace("term-db-debug") << n << " is already redundant." << std::endl; + //congruentCount++; + //alreadyCongruentCount++; + } + }else{ + Trace("term-db-debug") << n << " is not relevant." << std::endl; + //nonRelevantCount++; + } + } + + /* + if( Trace.isOn("term-db-index") ){ + Trace("term-db-index") << "Term index for " << f << " : " << std::endl; + Trace("term-db-index") << "- " << it->first << std::endl; + d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]); + Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = "; + Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; + } + */ + } + } +} + bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { + computeUfTerms( f ); Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r ); std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); if( it != d_func_map_rel_dom.end() ){ @@ -584,10 +667,10 @@ void TermDb::presolve() { } bool TermDb::reset( Theory::Effort effort ){ - int nonCongruentCount = 0; - int congruentCount = 0; - int alreadyCongruentCount = 0; - int nonRelevantCount = 0; + //int nonCongruentCount = 0; + //int congruentCount = 0; + //int alreadyCongruentCount = 0; + //int nonRelevantCount = 0; d_op_nonred_count.clear(); d_arg_reps.clear(); d_func_map_trie.clear(); @@ -642,71 +725,16 @@ bool TermDb::reset( Theory::Effort effort ){ } } +/* //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - d_op_nonred_count[ it->first ] = 0; - Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl; - for( unsigned i=0; isecond.size(); i++ ){ - Node n = it->second[i]; - //to be added to term index, term must be relevant, and exist in EE - if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ - if( isTermActive( n ) ){ - if( options::finiteModelFind() ){ - computeModelBasisArgAttribute( n ); - } - computeArgReps( n ); - - Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; - for( unsigned i=0; ifirst][i].begin(), - d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){ - d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] ); - } - } - Trace("term-db-debug") << std::endl; - Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; - Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] ); - Trace("term-db-debug2") << "...add term returned " << at << std::endl; - if( at!=n && ee->areEqual( at, n ) ){ - setTermInactive( n ); - Trace("term-db-debug") << n << " is redundant." << std::endl; - congruentCount++; - }else{ - if( at!=n && ee->areDisequal( at, n, false ) ){ - std::vector< Node > lits; - lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) ); - for( unsigned i=0; imkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() ); - } - } - Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); - if( Trace.isOn("term-db-lemma") ){ - Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; - if( !d_quantEngine->getTheoryEngine()->needCheck() ){ - Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; - } - Trace("term-db-lemma") << " add lemma : " << lem << std::endl; - } - d_quantEngine->addLemma( lem ); - d_consistent_ee = false; - return false; - } - nonCongruentCount++; - d_op_nonred_count[ it->first ]++; - } - }else{ - Trace("term-db-debug") << n << " is already redundant." << std::endl; - congruentCount++; - alreadyCongruentCount++; - } - }else{ - Trace("term-db-debug") << n << " is not relevant." << std::endl; - nonRelevantCount++; - } + computeUfTerms( it->first ); + if( !d_consistent_ee ){ + return false; } } +*/ + /* Trace("term-db-stats") << "TermDb: Reset" << std::endl; Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = "; Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; @@ -719,10 +747,12 @@ bool TermDb::reset( Theory::Effort effort ){ } } } + */ return true; } TermArgTrie * TermDb::getTermArgTrie( Node f ) { + computeUfTerms( f ); std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); if( itut!=d_func_map_trie.end() ){ return &itut->second; @@ -751,11 +781,18 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) { } TNode TermDb::getCongruentTerm( Node f, Node n ) { - computeArgReps( n ); - return d_func_map_trie[f].existsTerm( d_arg_reps[n] ); + computeUfTerms( f ); + std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); + if( itut!=d_func_map_trie.end() ){ + computeArgReps( n ); + return itut->second.existsTerm( d_arg_reps[n] ); + }else{ + return TNode::null(); + } } TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { + computeUfTerms( f ); return d_func_map_trie[f].existsTerm( args ); } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 004292622..684b6cf83 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -248,6 +248,8 @@ public: void computeArgReps( TNode n ); /** compute uf eqc terms */ void computeUfEqcTerms( TNode f ); + /** compute uf terms */ + void computeUfTerms( TNode f ); /** in relevant domain */ bool inRelevantDomain( TNode f, unsigned i, TNode r ); /** evaluate a term under a substitution. Return representative in EE if possible. @@ -271,7 +273,7 @@ public: Node getEligibleTermInEqc( TNode r ); /** is inst closure */ bool isInstClosure( Node r ); - + //for model basis private: //map from types to model basis terms diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2451036f1..12edb5277 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -353,7 +353,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ std::vector< QuantifiersModule* > qm; if( d_model->checkNeeded() ){ needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call - for( int i=0; i<(int)d_modules.size(); i++ ){ + for( unsigned i=0; ineedsCheck( e ) ){ qm.push_back( d_modules[i] ); needsCheck = true; @@ -396,6 +396,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ } d_recorded_inst.clear(); } + + double clSet = 0; + if( Trace.isOn("quant-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl; + } if( Trace.isOn("quant-engine-debug") ){ Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl; @@ -456,7 +462,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ flushLemmas(); if( d_hasAddedLemma ){ return; - } if( e==Theory::EFFORT_LAST_CALL ){ @@ -548,6 +553,13 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } } + if( Trace.isOn("quant-engine") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet); + Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma; + Trace("quant-engine") << std::endl; + } + Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl; }else{ Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl; @@ -567,7 +579,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } if( setIncomplete ){ - Trace("quant-engine-debug") << "Set incomplete flag." << std::endl; + Trace("quant-engine") << "Set incomplete flag." << std::endl; getOutputChannel().setIncomplete(); } //output debug stats @@ -646,8 +658,6 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ d_modules[i]->registerQuantifier( f ); } Node ceBody = d_term_db->getInstConstantBody( f ); - //generate the phase requirements - //d_phase_reqs[f] = new QuantPhaseReq( ceBody, true ); //also register it with the strong solver //if( options::finiteModelFind() ){ // ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); @@ -1209,9 +1219,19 @@ quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() { void QuantifiersEngine::flushLemmas(){ if( !d_lemmas_waiting.empty() ){ + //filter based on notify classes + if( !d_inst_notify.empty() ){ + unsigned prev_lem_sz = d_lemmas_waiting.size(); + for( unsigned j=0; jfilterInstantiations(); + } + if( prev_lem_sz!=d_lemmas_waiting.size() ){ + Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl; + } + } //take default output channel if none is provided d_hasAddedLemma = true; - for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){ + for( unsigned i=0; i& terms, Node body ) = 0; + virtual void filterInstantiations() = 0; }; namespace quantifiers { diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 2ca807662..8c847be60 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -48,7 +48,8 @@ TESTS = commutative.sy \ clock-inc-tuple.sy \ dt-test-ns.sy \ no-mention.sy \ - max2-univ.sy + max2-univ.sy \ + strings-small.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy new file mode 100644 index 000000000..bc559f94a --- /dev/null +++ b/test/regress/regress0/sygus/strings-small.sy @@ -0,0 +1,35 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si --no-dump-synth +(set-logic SLIA) +(synth-fun f ((firstname String) (lastname String)) String +((Start String (ntString)) + +(ntString String ( +firstname +lastname +" " +(str.++ ntString ntString))) + +(ntInt Int ( +0 +1 +2 +(+ ntInt ntInt) +(- ntInt ntInt) +(str.len ntString) +(str.to.int ntString) +(str.indexof ntString ntString ntInt))) + +(ntBool Bool ( +true +false +(str.prefixof ntString ntString) +(str.suffixof ntString ntString) +(str.contains ntString ntString))) + +)) + +(constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer")) + +(check-synth) + -- 2.30.2