From b9edba75ed506427502c9d565152794669e3ae23 Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Mon, 7 Mar 2016 14:30:36 -0600 Subject: [PATCH] modified CVC4 native language parser to accept 1-tuple declaration: TUPLE(1) - fixed the tuple element selection for product-split and join-split rules --- src/parser/cvc/Cvc.g | 30 +++++++++---- src/theory/sets/theory_sets_rels.cpp | 65 ++++++++++++++-------------- src/theory/sets/theory_sets_rels.h | 2 +- 3 files changed, 55 insertions(+), 42 deletions(-) diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3991da886..27182cb6d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -109,6 +109,8 @@ tokens { SUBTYPE_TOK = 'SUBTYPE'; SET_TOK = 'SET'; + + TUPLE_TOK = 'TUPLE'; FORALL_TOK = 'FORALL'; EXISTS_TOK = 'EXISTS'; @@ -294,6 +296,7 @@ int getOperatorPrecedence(int type) { case STAR_TOK: case INTDIV_TOK: case DIV_TOK: + case TUPLE_TOK: case MOD_TOK: return 23; case PLUS_TOK: case MINUS_TOK: @@ -1212,8 +1215,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, | ARRAY_TOK restrictedType[t,check] OF_TOK restrictedType[t2,check] { t = EXPR_MANAGER->mkArrayType(t, t2); } | SET_TOK OF_TOK restrictedType[t,check] - { t = EXPR_MANAGER->mkSetType(t); } - + { t = EXPR_MANAGER->mkSetType(t); } + /* subtypes */ | SUBTYPE_TOK LPAREN /* A bit tricky: this LAMBDA expression cannot refer to constants @@ -1644,9 +1647,19 @@ bvNegTerm[CVC4::Expr& f] : BVNEG_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } | TRANSPOSE_TOK bvNegTerm[f] - { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } + { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } | TRANSCLOSURE_TOK bvNegTerm[f] - { f = MK_EXPR(CVC4::kind::TRANSCLOSURE, f); } + { f = MK_EXPR(CVC4::kind::TRANSCLOSURE, f); } + | TUPLE_TOK LPAREN bvNegTerm[f] RPAREN + { std::vector types; + std::vector args; + args.push_back(f); + types.push_back(f.getType()); + DatatypeType t = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = t.getDatatype(); + args.insert( args.begin(), dt[0].getConstructor() ); + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); + } | postfixTerm[f] ; @@ -1959,8 +1972,8 @@ simpleTerm[CVC4::Expr& f] Type t, t2; } /* if-then-else */ - : iteTerm[f] - + : iteTerm[f] + /* parenthesized sub-formula / tuple literals */ | LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RPAREN @@ -1977,14 +1990,15 @@ simpleTerm[CVC4::Expr& f] args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } - } + } /* empty tuple literal */ | LPAREN RPAREN { std::vector types; DatatypeType t = EXPR_MANAGER->mkTupleType(types); const Datatype& dt = t.getDatatype(); - f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } + /* empty record literal */ | PARENHASH HASHPAREN { DatatypeType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair >()); diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index f8a4d009d..4530e3879 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -114,7 +114,7 @@ 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] rep is a var?? + // Todo: check n[0] or n[0]'s rep is a var?? if(tup_rep.isVar() && d_symbolic_tuples.find(tup_rep) == d_symbolic_tuples.end()) { std::vector tuple_elements; tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor())); @@ -123,7 +123,7 @@ typedef std::map >::iterator mem_it; } Node unfold_membership = MEMBER(NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements), n[1]); Node tuple_unfold_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, unfold_membership); - sendLemma(tuple_unfold_lemma, d_trueNode, "tuple-unfold"); + sendLemma(tuple_unfold_lemma, d_trueNode, "tuple-instantiate"); d_symbolic_tuples.insert(tup_rep); } computeTupleReps(tup_rep); @@ -190,21 +190,22 @@ typedef std::map >::iterator mem_it; << " with explaination: " << exp << std::endl; std::vector r1_element; std::vector r2_element; - Node::iterator child_it = atom[0].begin(); + NodeManager *nm = NodeManager::currentNM(); Datatype dt = r1_rep.getType().getSetElementType().getDatatype(); + unsigned int i = 0; unsigned int s1_len = r1_rep.getType().getSetElementType().getTupleLength(); + unsigned int tup_len = product_term.getType().getSetElementType().getTupleLength(); r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); - for(unsigned int i = 0; i < s1_len; ++child_it) { - r1_element.push_back(*child_it); - ++i; + for(; i < s1_len; ++i) { + r1_element.push_back(selectElement(atom[0], i)); } dt = r2_rep.getType().getSetElementType().getDatatype(); r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); - for(; child_it != atom[0].end(); ++child_it) { - r2_element.push_back(*child_it); + for(; i < tup_len; ++i) { + r2_element.push_back(selectElement(atom[0], i)); } Node fact; @@ -260,26 +261,27 @@ typedef std::map >::iterator mem_it; std::vector r1_element; std::vector r2_element; - Node::iterator child_it = atom[0].begin(); NodeManager *nm = NodeManager::currentNM(); TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0]; Node shared_x = nm->mkSkolem("sde_", shared_type); Datatype dt = r1_rep.getType().getSetElementType().getDatatype(); + unsigned int i = 0; unsigned int s1_len = r1_rep.getType().getSetElementType().getTupleLength(); + unsigned int tup_len = join_term.getType().getSetElementType().getTupleLength(); r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); - for(unsigned int i = 0; i < s1_len-1; ++child_it, ++i) { - r1_element.push_back(*child_it); + for(; i < s1_len-1; ++i) { + r1_element.push_back(selectElement(atom[0], i)); } r1_element.push_back(shared_x); + dt = r2_rep.getType().getSetElementType().getDatatype(); r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); r2_element.push_back(shared_x); - for(; child_it != atom[0].end(); ++child_it) { - r2_element.push_back(*child_it); + for(; i < tup_len; ++i) { + r2_element.push_back(selectElement(atom[0], i)); } - Node t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element); Node t2 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element); computeTupleReps(t1); @@ -347,7 +349,7 @@ typedef std::map >::iterator mem_it; Node fact = MEMBER(reversedTuple, tp_t0_rep); if(!polarity) { - // tp_term is a nested term + // tp_term is a nested term and we eagerly compute its subterms' members if(d_terms_cache[tp_t0_rep].find(kind::JOIN) != d_terms_cache[tp_t0_rep].end()) { std::vector join_terms = d_terms_cache[tp_t0_rep][kind::JOIN]; @@ -473,9 +475,6 @@ typedef std::map >::iterator mem_it; std::vector r2_exps = d_membership_exp_cache[r2_rep]; Node new_rel = n.getKind() == kind::JOIN ? nm->mkNode(kind::JOIN, r1_rep, r2_rep) : nm->mkNode(kind::PRODUCT, r1_rep, r2_rep); - Trace("rels-debug") << "[sets-rels] elements sizes: " - << r1_elements.size() << " and " << r2_elements.size() - << " " << r1_elements[0] << " and " << r2_elements[0]<< std::endl; Node new_rel_rep = getRepresentative(new_rel); unsigned int t1_len = r1_elements.front().getType().getTupleLength(); @@ -488,9 +487,7 @@ typedef std::map >::iterator mem_it; Node r2_lmost = selectElement(r2_elements[j], 0); Node r1_rmost = selectElement(r1_elements[i], t1_len-1); composed_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); - Trace("rels-debug") << "[sets-rels$$$$$$] r2_elements[j] = "<< r2_elements[j] << " is const? " << r2_elements[j].isConst() - << " is Var? " << r2_elements[j].isVar() - << " r1_element equal to r2_element? " << areEqual(r1_rmost, r2_lmost) << std::endl; + if((areEqual(r1_rmost, r2_lmost) && n.getKind() == kind::JOIN) || n.getKind() == kind::PRODUCT) { unsigned int k = 0; @@ -525,7 +522,7 @@ typedef std::map >::iterator mem_it; } Node reason = Rewriter::rewrite(nm->mkNode(kind::AND, reasons)); if(safeAddToMap(d_membership_db, new_rel_rep, composed_tuple_node)) { - safeAddToMap(d_membership_exp_cache, new_rel_rep, reason); + addToMap(d_membership_exp_cache, new_rel_rep, reason); } Trace("rels-debug") << "[sets-rels] compose tuples: " << r1_elements[i] << " and " << r2_elements[j] @@ -549,7 +546,7 @@ typedef std::map >::iterator mem_it; d_membership_db[new_rel_rep] = new_tups; d_membership_exp_cache[new_rel_rep] = new_exps; } - Trace("rels-debug") << "[sets-rels] Done with joining tuples !" << std::endl; + Trace("rels-debug") << "[sets-rels] Done with composing tuples !" << std::endl; } void TheorySetsRels::doPendingLemmas() { @@ -596,7 +593,7 @@ typedef std::map >::iterator mem_it; void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) { Trace("rels-lemma") << "[sets-lemma] Infer " << conc << " from " << ant << " by " << c << std::endl; d_lemma_cache.push_back(conc); -// d_lemma.push_back(conc); + d_lemma.push_back(conc); } void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) { @@ -688,11 +685,7 @@ typedef std::map >::iterator mem_it; } bool TheorySetsRels::areEqual( Node a, Node b ){ - Trace("rels-debug") << "[sets-rel] compare the equality of a = " << a - << " and b = " << b << std::endl; if( hasTerm( a ) && hasTerm( b ) ){ - Trace("rels-debug") << "[sets-rel] ********* has term a = " << a - << " and b = " << b << std::endl; // if( d_eqEngine->isTriggerTerm(a, THEORY_SETS) && // d_eqEngine->isTriggerTerm(b, THEORY_SETS) ) { // // Get representative trigger terms @@ -791,11 +784,16 @@ typedef std::map >::iterator mem_it; bool polarity = node.getKind() != kind::NOT; Node atom = polarity ? node : node[0]; Node polarity_atom = polarity ? d_trueNode : d_falseNode; - Node atom_mod = NodeManager::currentNM()->mkNode(atom.getKind(), getRepresentative(atom[0]), - getRepresentative(atom[1]) ); - //Trace("rels-lemma-compare-element") << "[sets-rels*******] atom_mod = " << atom_mod << std::endl; - d_eqEngine->addTerm(atom_mod); - return areEqual(atom_mod, polarity_atom); + if(d_eqEngine->hasTerm(node)) { + return areEqual(node, polarity_atom); + } else { + Node atom_mod = NodeManager::currentNM()->mkNode(atom.getKind(), getRepresentative(atom[0]), + getRepresentative(atom[1]) ); + if(d_eqEngine->hasTerm(atom_mod)) { + return areEqual(node, polarity_atom); + } + } + return false; } void TheorySetsRels::computeTupleReps( Node n ) { @@ -816,6 +814,7 @@ typedef std::map >::iterator mem_it; d_falseNode(NodeManager::currentNM()->mkConst(false)), d_infer(c), d_infer_exp(c), + d_lemma(c), d_eqEngine(eq), d_conflict(conflict) { diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index b297a25d3..077e950e3 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -73,7 +73,7 @@ private: /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeList d_infer; NodeList d_infer_exp; -// NodeList d_lemma; + NodeList d_lemma; std::map< Node, std::vector > d_tuple_reps; std::map< Node, TupleTrie > d_membership_trie; -- 2.30.2