From: PaulMeng Date: Thu, 10 Mar 2016 20:34:26 +0000 (-0600) Subject: fixed the transpose-occur rule X-Git-Tag: cvc5-1.0.0~6070 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=378a4df93162fe8e673f5cff42f38c20a872a646;p=cvc5.git fixed the transpose-occur rule --- diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 11667f850..564b33089 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -53,39 +53,52 @@ typedef std::map >::iterator mem_it; void TheorySetsRels::check() { mem_it m_it = d_membership_cache.begin(); while(m_it != d_membership_cache.end()) { - std::vector tuples = m_it->second; + Node rel_rep = m_it->first; // No relational terms found with rel_rep as its representative if(d_terms_cache.find(rel_rep) == d_terms_cache.end()) { + // TRANSPOSE(rel_rep) may occur in the context + Node tp_rel = NodeManager::currentNM()->mkNode(kind::TRANSPOSE, rel_rep); + Node tp_rel_rep = getRepresentative(tp_rel); + if(d_terms_cache.find(tp_rel_rep) != d_terms_cache.end()) { + std::vector tuples = m_it->second; + for(unsigned int i = 0; i < tuples.size(); i++) { + Node exp = tp_rel == tp_rel_rep ? d_membership_exp_cache[rel_rep][i] + : AND(d_membership_exp_cache[rel_rep][i], EQUAL(tp_rel, tp_rel_rep)); + // Lazily apply transpose-occur rule. + // Need to eagerly apply if we don't send facts as lemmas + applyTransposeRule(exp, tp_rel_rep, true); + } + } m_it++; continue; } + + std::vector tuples = m_it->second; for(unsigned int i = 0; i < tuples.size(); i++) { - Node tup_rep = tuples[i]; Node exp = d_membership_exp_cache[rel_rep][i]; std::map > kind_terms = d_terms_cache[rel_rep]; if(kind_terms.find(kind::TRANSPOSE) != kind_terms.end()) { - std::vector tp_terms = kind_terms.at(kind::TRANSPOSE); + std::vector tp_terms = kind_terms[kind::TRANSPOSE]; // exp is a membership term and tp_terms contains all // transposed terms that are equal to the right hand side of exp for(unsigned int j = 0; j < tp_terms.size(); j++) { - applyTransposeRule(exp, rel_rep, tp_terms[j]); + applyTransposeRule(exp, tp_terms[j]); } } if(kind_terms.find(kind::JOIN) != kind_terms.end()) { - std::vector conj; - std::vector join_terms = kind_terms.at(kind::JOIN); + std::vector join_terms = kind_terms[kind::JOIN]; // exp is a membership term and join_terms contains all - // joined terms that are in the same equivalence class with the right hand side of exp + // terms involving "join" operator that are in the same equivalence class with the right hand side of exp for(unsigned int j = 0; j < join_terms.size(); j++) { - applyJoinRule(exp, rel_rep, join_terms[j]); + applyJoinRule(exp, join_terms[j]); } } if(kind_terms.find(kind::PRODUCT) != kind_terms.end()) { - std::vector product_terms = kind_terms.at(kind::PRODUCT); + std::vector product_terms = kind_terms[kind::PRODUCT]; for(unsigned int j = 0; j < product_terms.size(); j++) { - applyProductRule(exp, rel_rep, product_terms[j]); + applyProductRule(exp, product_terms[j]); } } } @@ -114,22 +127,8 @@ typedef std::map >::iterator mem_it; Node tup_rep = getRepresentative(n[0]); Node rel_rep = getRepresentative(n[1]); // Todo: check n[0] or n[0]'s rep is a var?? - if(n[0].isVar()) { - if(d_symbolic_tuples.find(n[0]) == d_symbolic_tuples.end()) { - std::vector tuple_elements; - tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor())); - for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) { - Node element = selectElement(n[0], i); - makeSharedTerm(element); - tuple_elements.push_back(element); - } - Node concrete_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); - concrete_tuple = MEMBER(concrete_tuple, n[1]); - Node concrete_tuple_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, concrete_tuple); - sendLemma(concrete_tuple_lemma, d_trueNode, "tuple-concretize"); - d_symbolic_tuples.insert(n[0]); - } - // not put symbolic tuple var in the membership exp map if possible + if(n[0].isVar()){ + reduceTupleVar(n); } else { if(safeAddToMap(d_membership_cache, rel_rep, tup_rep)) { bool true_eq = areEqual(r, d_trueNode); @@ -167,6 +166,14 @@ typedef std::map >::iterator mem_it; } } } + // need to add all tuple elements as shared terms + } else if(n.getType().isTuple() && !n.isConst() && !n.isVar()) { + for(unsigned int i = 0; i < n.getType().getTupleLength(); i++) { + Node element = selectElement(n, i); + if(!element.isConst()) { + makeSharedTerm(element); + } + } } ++eqc_i; } @@ -184,13 +191,13 @@ typedef std::map >::iterator mem_it; * (a, b, c, d) IS_IN (X PRODUCT Y) */ - void TheorySetsRels::applyProductRule(Node exp, Node rel_rep, Node product_term) { + void TheorySetsRels::applyProductRule(Node exp, Node product_term) { bool polarity = exp.getKind() != kind::NOT; Node atom = polarity ? exp : exp[0]; Node r1_rep = getRepresentative(product_term[0]); Node r2_rep = getRepresentative(product_term[1]); - if(polarity) { + if(polarity & d_lemma.find(exp) != d_lemma.end()) { Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT-SPLIT rule on term: " << product_term << " with explaination: " << exp << std::endl; std::vector r1_element; @@ -252,13 +259,13 @@ typedef std::map >::iterator mem_it; * ------------------------------------------------------------- * (a, c) IS_IN (X JOIN Y) */ - void TheorySetsRels::applyJoinRule(Node exp, Node rel_rep, Node join_term) { + void TheorySetsRels::applyJoinRule(Node exp, Node join_term) { bool polarity = exp.getKind() != kind::NOT; Node atom = polarity ? exp : exp[0]; Node r1_rep = getRepresentative(join_term[0]); Node r2_rep = getRepresentative(join_term[1]); - if(polarity) { + if(polarity && d_lemma.find(exp) != d_lemma.end()) { Trace("rels-debug") << "\n[sets-rels] Apply JOIN-SPLIT rule on term: " << join_term << " with explaination: " << exp << std::endl; @@ -309,14 +316,14 @@ typedef std::map >::iterator mem_it; fact = MEMBER(t1, r1_rep); if(r1_rep != join_term[0]) reasons = Rewriter::rewrite(AND(reason, EQUAL(r1_rep, join_term[0]))); - produceNewMembership(r1_rep, t1, reasons); + addToMembershipDB(r1_rep, t1, reasons); sendInfer(fact, reasons, "join-split"); reasons = reason; fact = MEMBER(t2, r2_rep); if(r2_rep != join_term[1]) reasons = Rewriter::rewrite(AND(reason, EQUAL(r2_rep, join_term[1]))); - produceNewMembership(r2_rep, t2, reasons); + addToMembershipDB(r2_rep, t2, reasons); sendInfer(fact, reasons, "join-split"); // Need to make the skolem "shared_x" as shared term @@ -330,20 +337,32 @@ typedef std::map >::iterator mem_it; } /* - * transpose rule: (a, b) IS_IN X NOT (t, u) IS_IN (TRANSPOSE X) - * ------------------------------------------------ - * (b, a) IS_IN (TRANSPOSE X) + * transpose-occur rule: [NOT] (a, b) IS_IN X [NOT] (t, u) IS_IN (TRANSPOSE X) + * ------------------------------------------------------- + * [NOT] (b, a) IS_IN (TRANSPOSE X) * * transpose rule: [NOT] (a, b) IS_IN (TRANSPOSE X) * ------------------------------------------------ * [NOT] (b, a) IS_IN X */ - void TheorySetsRels::applyTransposeRule(Node exp, Node rel_rep, Node tp_term) { + void TheorySetsRels::applyTransposeRule(Node exp, Node tp_term, bool tp_occur_rule) { Trace("rels-debug") << "\n[sets-rels] Apply transpose rule on term: " << tp_term << " with explaination: " << exp << std::endl; bool polarity = exp.getKind() != kind::NOT; Node atom = polarity ? exp : exp[0]; Node reversedTuple = getRepresentative(reverseTuple(atom[0])); + if(tp_occur_rule) { + Node fact = polarity ? MEMBER(reversedTuple, tp_term) : MEMBER(reversedTuple, tp_term).negate(); + if(holds(fact)) { + Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds. Skip...." << std::endl; + } else { + sendInfer(fact, exp, "transpose-occur"); + if(polarity) { + addToMembershipDB(tp_term, reversedTuple, exp); + } + } + return; + } Node tp_t0_rep = getRepresentative(tp_term[0]); Node reason = atom[1] == tp_term ? exp : Rewriter::rewrite(AND(exp, EQUAL(atom[1], tp_term))); Node fact = MEMBER(reversedTuple, tp_t0_rep); @@ -371,7 +390,7 @@ typedef std::map >::iterator mem_it; } else { sendInfer(fact, reason, "transpose-rule"); if(polarity) { - produceNewMembership(tp_t0_rep, reversedTuple, reason); + addToMembershipDB(tp_t0_rep, reversedTuple, reason); } } } @@ -437,7 +456,7 @@ typedef std::map >::iterator mem_it; if(holds(fact)) { Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds! Skip..." << std::endl; } else { - produceNewMembership(n_rep, rev_tup, Rewriter::rewrite(reason)); + addToMembershipDB(n_rep, rev_tup, Rewriter::rewrite(reason)); sendInfer(fact, Rewriter::rewrite(reason), "transpose-rule"); } } @@ -515,7 +534,7 @@ typedef std::map >::iterator mem_it; } Node reason = Rewriter::rewrite(nm->mkNode(kind::AND, reasons)); - produceNewMembership(new_rel_rep, composed_tuple_rep, reason); + addToMembershipDB(new_rel_rep, composed_tuple_rep, reason); if(isProduct) sendInfer( fact, reason, "product-compose" ); @@ -581,7 +600,7 @@ typedef std::map >::iterator mem_it; Trace("rels-lemma") << "[sets-lemma] Infer " << conc << " from " << ant << " by " << c << std::endl; Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); d_lemma_cache.push_back(lemma); - d_lemma.push_back(lemma); + d_lemma.insert(lemma); } void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) { @@ -792,13 +811,31 @@ typedef std::map >::iterator mem_it; } } - void TheorySetsRels::produceNewMembership(Node rel, Node member, Node reasons) { + inline void TheorySetsRels::addToMembershipDB(Node rel, Node member, Node reasons) { addToMap(d_membership_db, rel, member); addToMap(d_membership_exp_db, rel, reasons); computeTupleReps(member); d_membership_trie[rel].addTerm(member, d_tuple_reps[member]); } + void TheorySetsRels::reduceTupleVar(Node n) { + if(d_symbolic_tuples.find(n[0]) == d_symbolic_tuples.end()) { + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one " << std::endl; + std::vector tuple_elements; + tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor())); + for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) { + Node element = selectElement(n[0], i); + makeSharedTerm(element); + tuple_elements.push_back(element); + } + Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); + tuple_reduct = MEMBER(tuple_reduct, n[1]); + Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, tuple_reduct); + sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); + d_symbolic_tuples.insert(n[0]); + } + } + TheorySetsRels::TheorySetsRels(context::Context* c, context::UserContext* u, eq::EqualityEngine* eq, @@ -809,7 +846,7 @@ typedef std::map >::iterator mem_it; d_falseNode(NodeManager::currentNM()->mkConst(false)), d_infer(c), d_infer_exp(c), - d_lemma(c), + d_lemma(u), d_eqEngine(eq), d_conflict(conflict) { @@ -843,6 +880,26 @@ typedef std::map >::iterator mem_it; } } +// void TupleTrie::findTerms( std::vector< Node >& reps, std::vector< Node >& elements, int argIndex ) { +// std::map< Node, TupleTrie >::iterator it; +// if( argIndex==(int)reps.size()-1 ){ +// if(reps[argIndex].getKind() == kind::SKOLEM) { +// it = d_data.begin(); +// while(it != d_data.end()) { +// elements.push_back(it->first); +// it++; +// } +// } +// }else{ +// it = d_data.find( reps[argIndex] ); +// if( it==d_data.end() ){ +// return ; +// }else{ +// it->second.findTerms( reps, argIndex+1 ); +// } +// } +// } + Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) { if( argIndex==(int)reps.size() ){ if( d_data.empty() ){ diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 9b3678d01..bd4d7fe64 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -36,6 +36,7 @@ public: public: Node existsTerm( std::vector< Node >& reps, int argIndex = 0 ); std::vector findTerms( std::vector< Node >& reps, int argIndex = 0 ); +// void findTerms( std::vector< Node >& reps, std::vector< Node >& elements, int argIndex = 0 ); bool addTerm( Node n, std::vector< Node >& reps, int argIndex = 0 ); void debugPrint( const char * c, Node n, unsigned depth = 0 ); void clear() { d_data.clear(); } @@ -74,7 +75,7 @@ private: /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeList d_infer; NodeList d_infer_exp; - NodeList d_lemma; + NodeSet d_lemma; std::map< Node, std::vector > d_tuple_reps; std::map< Node, TupleTrie > d_membership_trie; @@ -93,9 +94,9 @@ private: void collectRelsInfo(); void assertMembership( Node fact, Node reason, bool polarity ); void composeTuplesForRels( Node ); - void applyTransposeRule( Node, Node, Node ); - void applyJoinRule( Node, Node, Node ); - void applyProductRule( Node, Node, Node ); + void applyTransposeRule( Node, Node, bool tp_occur_rule = false ); + void applyJoinRule( Node, Node ); + void applyProductRule( Node, Node ); void computeRels( Node ); void computeTransposeRelations( Node ); Node reverseTuple( Node ); @@ -119,7 +120,8 @@ private: bool holds( Node ); void computeTupleReps( Node ); void makeSharedTerm( Node ); - inline void produceNewMembership( Node, Node, Node ); + void reduceTupleVar( Node ); + inline void addToMembershipDB( Node, Node, Node ); }; diff --git a/test/regress/regress0/sets/rels/rel_complex_1.cvc b/test/regress/regress0/sets/rels/rel_complex_1.cvc deleted file mode 100644 index 969d0d71c..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_1.cvc +++ /dev/null @@ -1,34 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; - -w : SET OF IntTup; -z : SET OF IntTup; -r2 : SET OF IntPair; - -a : IntPair; -ASSERT a = (3,1); -ASSERT a IS_IN x; - -d : IntPair; -ASSERT d = (1,3); -ASSERT d IS_IN y; - -e : IntPair; -ASSERT e = (4,3); -ASSERT r = (x JOIN y); - -ASSERT TUPLE(1) IS_IN w; -ASSERT TUPLE(2) IS_IN z; -ASSERT r2 = (w PRODUCT z); - -ASSERT NOT (e IS_IN r); -%ASSERT e IS_IN r2; -ASSERT (r <= r2); -ASSERT NOT ((3,3) IS_IN r2); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_complex_3.cvc b/test/regress/regress0/sets/rels/rel_complex_3.cvc new file mode 100644 index 000000000..492c94432 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_3.cvc @@ -0,0 +1,49 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +w : SET OF IntPair; + + +f : IntPair; +ASSERT f = (3,1); +ASSERT f IS_IN x; + +g : IntPair; +ASSERT g = (1,3); +ASSERT g IS_IN y; + +h : IntPair; +ASSERT h = (3,5); +ASSERT h IS_IN x; +ASSERT h IS_IN y; + +ASSERT r = (x JOIN y); + +e : IntPair; + +ASSERT NOT (e IS_IN r); +ASSERT NOT(z = (x & y)); +ASSERT z = (x - y); +ASSERT x <= y; +ASSERT e IS_IN (r JOIN z); +ASSERT e IS_IN x; +ASSERT e IS_IN (x & y); +CHECKSAT TRUE; + + + + + + + + + + + + + + diff --git a/test/regress/regress0/sets/rels/rel_complex_4.cvc b/test/regress/regress0/sets/rels/rel_complex_4.cvc new file mode 100644 index 000000000..f473b00aa --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_4.cvc @@ -0,0 +1,52 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +w : SET OF IntPair; + + +f : IntPair; +ASSERT f = (3,1); +ASSERT f IS_IN x; + +g : IntPair; +ASSERT g = (1,3); +ASSERT g IS_IN y; + +h : IntPair; +ASSERT h = (3,5); +ASSERT h IS_IN x; +ASSERT h IS_IN y; + +ASSERT r = (x JOIN y); +a:INT; +e : IntPair; +ASSERT e = (a,a); +ASSERT w = {e}; +ASSERT TRANSPOSE(w) <= y; + +ASSERT NOT (e IS_IN r); +ASSERT NOT(z = (x & y)); +ASSERT z = (x - y); +ASSERT x <= y; +ASSERT e IS_IN (r JOIN z); +ASSERT e IS_IN x; +ASSERT e IS_IN (x & y); +CHECKSAT TRUE; + + + + + + + + + + + + + + diff --git a/test/regress/regress0/sets/rels/rel_join.cvc b/test/regress/regress0/sets/rels/rel_join.cvc deleted file mode 100644 index 7cce736f5..000000000 --- a/test/regress/regress0/sets/rels/rel_join.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; - -z : IntPair; -ASSERT z = (1,2); -zt : IntPair; -ASSERT zt = (2,1); -v : IntPair; -ASSERT v = (1,1); -a : IntPair; -ASSERT a = (1,5); - -ASSERT (1, 7) IS_IN x; -ASSERT (7, 5) IS_IN y; - -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -%ASSERT a IS_IN (x JOIN y); -%ASSERT NOT (v IS_IN (x JOIN y)); -ASSERT NOT (a IS_IN (x JOIN y)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_6.cvc b/test/regress/regress0/sets/rels/rel_join_6.cvc new file mode 100644 index 000000000..17318872f --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_6.cvc @@ -0,0 +1,13 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +ASSERT x = {(1,2), (3, 4)}; + +ASSERT y = (x JOIN {(2,1), (4,3)}); + +ASSERT NOT ((1,1) IS_IN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose.cvc b/test/regress/regress0/sets/rels/rel_transpose.cvc deleted file mode 100644 index 10644d794..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : IntPair; -ASSERT z = (1,2); -zt : IntPair; -ASSERT zt = (2,1); -ASSERT z IS_IN x; -ASSERT NOT (zt IS_IN (TRANSPOSE x)); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_2.cvc b/test/regress/regress0/sets/rels/rel_transpose_2.cvc deleted file mode 100644 index 15a035b58..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_2.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntTup: TYPE = [INT]; -x : SET OF IntTup; -y : SET OF IntTup; -z : IntTup; -ASSERT z = (1); -zt : IntTup; -ASSERT zt = (1); -ASSERT z IS_IN x; -ASSERT NOT (zt IS_IN (TRANSPOSE x)); -CHECKSAT;