TRANSPOSE_TOK = 'TRANSPOSE';
PRODUCT_TOK = 'PRODUCT';
TRANSCLOSURE_TOK = 'TCLOSURE';
+ IDEN_TOK = 'IDEN';
+ JOIN_IMAGE_TOK = 'JOIN_IMAGE';
// Strings
case JOIN_TOK:
case TRANSPOSE_TOK:
case PRODUCT_TOK:
+ case IDEN_TOK:
+ case JOIN_IMAGE_TOK:
case TRANSCLOSURE_TOK: return 24;
case LEQ_TOK:
case LT_TOK:
case PRODUCT_TOK: return kind::PRODUCT;
case JOIN_TOK: return kind::JOIN;
+ case JOIN_IMAGE_TOK: return kind::JOIN_IMAGE;
// comparisonBinop
case EQUAL_TOK: return kind::EQUAL;
| AND_TOK
| JOIN_TOK
| PRODUCT_TOK
+ | JOIN_IMAGE_TOK
;
comparison[CVC4::Expr& f]
const Datatype& dt = t.getDatatype();
args.insert( args.begin(), dt[0].getConstructor() );
f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
- }
+ }
+ | IDEN_TOK relationTerm[f]
+ { f = MK_EXPR(CVC4::kind::IDEN, f); }
| postfixTerm[f]
;
op << "TCLOSURE";
opType = PREFIX;
break;
+ case kind::IDEN:
+ op << "IDEN";
+ opType = PREFIX;
+ break;
+ case kind::JOIN_IMAGE:
+ op << "JOIN_IMAGE";
+ opType = INFIX;
+ break;
case kind::SINGLETON:
out << "{";
toStream(out, n[0], depth, types, false);
break;
case kind::INSERT: {
if(bracket) {
- out << '(';
+ out << '(';
}
out << '{';
size_t i = 0;
out << "} | ";
toStream(out, n[i], depth, types, true);
if(bracket) {
- out << ')';
+ out << ')';
}
return;
break;
operator PRODUCT 2 "set cartesian product"
operator TRANSPOSE 1 "set transpose"
operator TCLOSURE 1 "set transitive closure"
+operator JOIN_IMAGE 2 "set join image"
+operator IDEN 1 "set identity"
typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule
typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule
+typerule JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule
+typerule IDEN ::CVC4::theory::sets::RelIdenTypeRule
construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule
construle TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule
+construle JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule
+construle IDEN ::CVC4::theory::sets::RelIdenTypeRule
endtheory
if( kind_terms.find(kind::TRANSPOSE) != kind_terms.end() ) {
std::vector<Node> 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
if( tp_terms.size() > 0 ) {
applyTransposeRule( tp_terms );
applyTransposeRule( tp_terms[0], rel_rep, exp );
}
if( kind_terms.find(kind::JOIN) != kind_terms.end() ) {
std::vector<Node> join_terms = kind_terms[kind::JOIN];
- // exp is a membership term and join_terms contains all
- // 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( join_terms[j], rel_rep, exp );
}
applyTCRule( mem, tc_terms[j], rel_rep, exp );
}
}
+ if( kind_terms.find(kind::JOIN_IMAGE) != kind_terms.end() ) {
+ std::vector<Node> join_image_terms = kind_terms[kind::JOIN_IMAGE];
+ for( unsigned int j = 0; j < join_image_terms.size(); j++ ) {
+ applyJoinImageRule( mem, join_image_terms[j], exp );
+ }
+ }
+ if( kind_terms.find(kind::IDEN) != kind_terms.end() ) {
+ std::vector<Node> iden_terms = kind_terms[kind::IDEN];
+ for( unsigned int j = 0; j < iden_terms.size(); j++ ) {
+ applyIdenRule( mem, iden_terms[j], exp );
+ }
+ }
}
m_it++;
}
buildTCGraphForRel( *term_it );
term_it++;
}
-
+ } else if( k_t_it->first == kind::JOIN_IMAGE ) {
+ std::vector<Node>::iterator term_it = k_t_it->second.begin();
+ while( term_it != k_t_it->second.end() ) {
+ computeMembersForJoinImageTerm( *term_it );
+ term_it++;
+ }
+ } else if( k_t_it->first == kind::IDEN ) {
+ std::vector<Node>::iterator term_it = k_t_it->second.begin();
+ while( term_it != k_t_it->second.end() ) {
+ computeMembersForIdenTerm( *term_it );
+ term_it++;
+ }
}
k_t_it++;
}
Node eqc_rep = (*eqcs_i);
eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine );
- Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << std::endl;
+ Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl;
while( !eqc_i.isFinished() ){
Node eqc_node = (*eqc_i);
computeTupleReps(tup_rep);
d_membership_trie[rel_rep].addTerm(tup_rep, d_tuple_reps[tup_rep]);
}
- } else {
- if( safelyAddToMap(d_rReps_nonMemberReps_cache, rel_rep, tup_rep) ) {
- addToMap(d_rReps_nonMemberReps_exp_cache, rel_rep, reason);
- }
}
}
// collect relational terms info
} else if( eqc_rep.getType().isSet() && eqc_rep.getType().getSetElementType().isTuple() ) {
if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN ||
- eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ) {
+ eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ||
+ eqc_node.getKind() == kind::JOIN_IMAGE || eqc_node.getKind() == kind::IDEN ) {
std::vector<Node> terms;
std::map< kind::Kind_t, std::vector<Node> > rel_terms;
TERM_IT terms_it = d_terms_cache.find(eqc_rep);
Trace("rels-debug") << "[Theory::Rels] Done with collecting relational terms!" << std::endl;
}
+ /* JOIN-IMAGE UP : (x, x1) IS_IN R, ..., (x, xn) IS_IN R (R JOIN_IMAGE n)
+ * -------------------------------------------------------
+ * x IS_IN (R JOIN_IMAGE n) || NOT DISTINCT(x1, ... , xn)
+ *
+ */
+
+ void TheorySetsRels::computeMembersForJoinImageTerm( Node join_image_term ) {
+ Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for JoinImage Term = " << join_image_term << std::endl;
+ MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( getRepresentative( join_image_term[0] ) );
+
+ if( rel_mem_it == d_rReps_memberReps_cache.end() ) {
+ return;
+ }
+
+ Node join_image_rel = join_image_term[0];
+ std::hash_set< Node, NodeHashFunction > hasChecked;
+ Node join_image_rel_rep = getRepresentative( join_image_rel );
+ std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin();
+ MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep );
+ std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
+ unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
+
+ while( mem_rep_it != (*rel_mem_it).second.end() ) {
+ Node fst_mem_rep = RelsUtils::nthElementOfTuple( *mem_rep_it, 0 );
+
+ if( hasChecked.find( fst_mem_rep ) != hasChecked.end() ) {
+ ++mem_rep_it;
+ ++mem_rep_exp_it;
+ continue;
+ }
+ hasChecked.insert( fst_mem_rep );
+
+ Datatype dt = join_image_term.getType().getSetElementType().getDatatype();
+ Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER,
+ NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
+ Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
+ join_image_term);
+ if( holds( new_membership ) ) {
+ ++mem_rep_it;
+ ++mem_rep_exp_it;
+ continue;
+ }
+
+ std::vector< Node > reasons;
+ std::vector< Node > existing_members;
+ std::vector< Node >::iterator mem_rep_exp_it_snd = (*rel_mem_exp_it).second.begin();
+
+ while( mem_rep_exp_it_snd != (*rel_mem_exp_it).second.end() ) {
+ Node fst_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 0 );
+
+ if( areEqual( fst_mem_rep, fst_element_snd_mem ) ) {
+ bool notExist = true;
+ std::vector< Node >::iterator existing_mem_it = existing_members.begin();
+ Node snd_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 1 );
+
+ while( existing_mem_it != existing_members.end() ) {
+ if( areEqual( (*existing_mem_it), snd_element_snd_mem ) ) {
+ notExist = false;
+ break;
+ }
+ ++existing_mem_it;
+ }
+
+ if( notExist ) {
+ existing_members.push_back( snd_element_snd_mem );
+ reasons.push_back( *mem_rep_exp_it_snd );
+ if( fst_mem_rep != fst_element_snd_mem ) {
+ reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem_rep, fst_element_snd_mem ) );
+ }
+ if( join_image_rel != (*mem_rep_exp_it_snd)[1] ) {
+ reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it_snd)[1], join_image_rel ));
+ }
+ if( existing_members.size() == min_card ) {
+ if( min_card >= 2) {
+ new_membership = NodeManager::currentNM()->mkNode( kind::OR, new_membership, NodeManager::currentNM()->mkNode( kind::NOT, NodeManager::currentNM()->mkNode( kind::DISTINCT, existing_members ) ));
+ }
+ Assert(reasons.size() >= 1);
+ sendInfer( new_membership, reasons.size() > 1 ? NodeManager::currentNM()->mkNode( kind::AND, reasons) : reasons[0], "JOIN-IMAGE UP" );
+ break;
+ }
+ }
+ }
+ ++mem_rep_exp_it_snd;
+ }
+ ++mem_rep_it;
+ ++mem_rep_exp_it;
+ }
+ Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for JoinImage Term" << join_image_term << "*********** " << std::endl;
+ }
+
+ /* JOIN-IMAGE DOWN : (x) IS_IN (R JOIN_IMAGE n)
+ * -------------------------------------------------------
+ * (x, x1) IS_IN R .... (x, xn) IS_IN R DISTINCT(x1, ... , xn)
+ *
+ */
+
+ void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) {
+ Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term
+ << " with mem_rep = " << mem_rep << " and exp = " << exp << std::endl;
+ if( d_rel_nodes.find( join_image_term ) == d_rel_nodes.end() ) {
+ computeMembersForJoinImageTerm( join_image_term );
+ d_rel_nodes.insert( join_image_term );
+ }
+
+ Node join_image_rel = join_image_term[0];
+ Node join_image_rel_rep = getRepresentative( join_image_rel );
+ MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( join_image_rel_rep );
+ unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
+
+ if( rel_mem_it != d_rReps_memberReps_cache.end() ) {
+ if( d_membership_trie.find( join_image_rel_rep ) != d_membership_trie.end() ) {
+ computeTupleReps( mem_rep );
+ if( d_membership_trie[join_image_rel_rep].findSuccessors(d_tuple_reps[mem_rep]).size() >= min_card ) {
+ return;
+ }
+ }
+ }
+
+ Node reason = exp;
+ Node conclusion = d_trueNode;
+ std::vector< Node > distinct_skolems;
+ Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
+
+ if( exp[1] != join_image_term ) {
+ reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) );
+ }
+ for( unsigned int i = 0; i < min_card; i++ ) {
+ Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] );
+ distinct_skolems.push_back( skolem );
+ conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) );
+ }
+ if( distinct_skolems.size() >= 2 ) {
+ conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) );
+ }
+ sendInfer( conclusion, reason, "JOIN-IMAGE DOWN" );
+ Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl;
+
+ }
+
+
+ /* IDENTITY-DOWN : (x, y) IS_IN IDEN(R)
+ * -------------------------------------------------------
+ * x = y, (x IS_IN R)
+ *
+ */
+
+ void TheorySetsRels::applyIdenRule( Node mem_rep, Node iden_term, Node exp) {
+ Trace("rels-debug") << "\n[Theory::Rels] *********** applyIdenRule on " << iden_term
+ << " with mem_rep = " << mem_rep << " and exp = " << exp << std::endl;
+ if( d_rel_nodes.find( iden_term ) == d_rel_nodes.end() ) {
+ computeMembersForIdenTerm( iden_term );
+ d_rel_nodes.insert( iden_term );
+ }
+ Node reason = exp;
+ Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
+ Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
+ Datatype dt = iden_term[0].getType().getSetElementType().getDatatype();
+ Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] );
+
+ if( exp[1] != iden_term ) {
+ reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) );
+ }
+ sendInfer( NodeManager::currentNM()->mkNode( kind::AND, fact, NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem, snd_mem ) ), reason, "IDENTITY-DOWN" );
+ Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyIdenRule on " << iden_term << std::endl;
+ }
+
+ /* IDEN UP : (x) IS_IN R IDEN(R) IN T
+ * --------------------------------
+ * (x, x) IS_IN IDEN(R)
+ *
+ */
+
+ void TheorySetsRels::computeMembersForIdenTerm( Node iden_term ) {
+ Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for Iden Term = " << iden_term << std::endl;
+ Node iden_term_rel = iden_term[0];
+ Node iden_term_rel_rep = getRepresentative( iden_term_rel );
+
+ if( d_rReps_memberReps_cache.find( iden_term_rel_rep ) == d_rReps_memberReps_cache.end() ) {
+ return;
+ }
+
+ MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( iden_term_rel_rep );
+ std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
+
+ while( mem_rep_exp_it != (*rel_mem_exp_it).second.end() ) {
+ Node reason = *mem_rep_exp_it;
+ Node fst_exp_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it)[0], 0 );
+ Node new_mem = RelsUtils::constructPair( iden_term, fst_exp_mem, fst_exp_mem );
+
+ if( (*mem_rep_exp_it)[1] != iden_term_rel ) {
+ reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it)[1], iden_term_rel ) );
+ }
+ sendInfer( NodeManager::currentNM()->mkNode( kind::MEMBER, new_mem, iden_term ), reason, "IDENTITY-UP" );
+ ++mem_rep_exp_it;
+ }
+ Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for Iden Term = " << iden_term << std::endl;
+ }
+
+
/*
* Construct transitive closure graph for tc_rep based on the members of tc_r_rep
*/
if( cur_set != tc_graph.end() ) {
for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin();
set_it != cur_set->second.end(); set_it++ ) {
- Node new_pair = constructPair( tc_rel, cur_node_rep, *set_it );
+ Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it );
std::vector< Node > new_reasons( reasons );
new_reasons.push_back( rel_tc_graph_exps.find( new_pair )->second );
doTCInference( tc_rel, new_reasons, tc_graph, rel_tc_graph_exps, start_node_rep, *set_it, seen );
computeTupleReps(mem2);
std::vector<Node> elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[mem1]);
+
for(unsigned int j = 0; j < elements.size(); j++) {
std::vector<Node> new_tup;
new_tup.push_back(elements[j]);
}
}
- inline Node TheorySetsRels::constructPair(Node tc_rep, Node a, Node b) {
- Datatype dt = tc_rep.getType().getSetElementType().getDatatype();
- return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b);
- }
-
/*
* Node n[0] is a tuple variable, reduce n[0] to a concrete representation,
* which is (e1, ..., en) where e1, ... ,en are concrete elements of tuple n[0].
d_eqEngine->addFunctionKind(kind::JOIN);
d_eqEngine->addFunctionKind(kind::TRANSPOSE);
d_eqEngine->addFunctionKind(kind::TCLOSURE);
+ d_eqEngine->addFunctionKind(kind::JOIN_IMAGE);
+ d_eqEngine->addFunctionKind(kind::IDEN);
}
TheorySetsRels::~TheorySetsRels() {
}
}
+ std::vector<Node> TupleTrie::findSuccessors( std::vector< Node >& reps, int argIndex ) {
+ std::vector<Node> nodes;
+ std::map< Node, TupleTrie >::iterator it;
+
+ if( argIndex==(int)reps.size() ){
+ it = d_data.begin();
+ while(it != d_data.end()) {
+ nodes.push_back(it->first);
+ it++;
+ }
+ return nodes;
+ }else{
+ it = d_data.find( reps[argIndex] );
+ if( it==d_data.end() ){
+ return nodes;
+ }else{
+ return it->second.findSuccessors( reps, argIndex+1 );
+ }
+ }
+ }
+
Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) {
if( argIndex==(int)reps.size() ){
if( d_data.empty() ){
}
}
}
-
-
-
-
-
-
-
-
-
-
-
-
-
std::map< Node, TupleTrie > d_data;
public:
std::vector<Node> findTerms( std::vector< Node >& reps, int argIndex = 0 );
+ std::vector<Node> findSuccessors( std::vector< Node >& reps, int argIndex = 0 );
Node existsTerm( std::vector< Node >& reps, int argIndex = 0 );
bool addTerm( Node n, std::vector< Node >& reps, int argIndex = 0 );
void debugPrint( const char * c, Node n, unsigned depth = 0 );
class TheorySetsRels {
typedef context::CDChunkList< Node > NodeList;
- typedef context::CDChunkList< int > IdList;
- typedef context::CDHashMap< int, IdList* > IdListMap;
typedef context::CDHashSet< Node, NodeHashFunction > NodeSet;
- typedef context::CDHashMap< Node, bool, NodeHashFunction > NodeBoolMap;
- typedef context::CDHashMap< Node, NodeList*, NodeHashFunction > NodeListMap;
- typedef context::CDHashMap< Node, NodeSet*, NodeHashFunction > NodeSetMap;
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
public:
* d_not_mem tuples that are not members of this equivalence class
* d_tp is a node of kind TRANSPOSE (if any) in this equivalence class,
* d_pt is a node of kind PRODUCT (if any) in this equivalence class,
- * d_join is a node of kind JOIN (if any) in this equivalence class,
* d_tc is a node of kind TCLOSURE (if any) in this equivalence class,
*/
class EqcInfo
Node d_falseNode;
/** Facts and lemmas to be sent to EE */
- std::map< Node, Node > d_pending_facts;
- std::vector< Node > d_lemmas_out;
NodeList d_pending_merge;
-
- /** inferences: maintained to ensure ref count for internally introduced nodes */
NodeSet d_lemmas_produced;
NodeSet d_shared_terms;
+ std::vector< Node > d_lemmas_out;
+ std::map< Node, Node > d_pending_facts;
+
- /** Relations that have been applied JOIN, PRODUCT, TC composition rules */
std::hash_set< Node, NodeHashFunction > d_rel_nodes;
std::map< Node, std::vector<Node> > d_tuple_reps;
std::map< Node, TupleTrie > d_membership_trie;
/** Symbolic tuple variables that has been reduced to concrete ones */
std::hash_set< Node, NodeHashFunction > d_symbolic_tuples;
- /** Mapping between relation and its (non)member representatives */
- std::map< Node, std::vector<Node> > d_rReps_memberReps_cache;
- std::map< Node, std::vector<Node> > d_rReps_nonMemberReps_cache;
-
-
- /** Mapping between relation and its (non)member representatives explanation */
- std::map< Node, std::vector<Node> > d_rReps_memberReps_exp_cache;
- std::map< Node, std::vector<Node> > d_rReps_nonMemberReps_exp_cache;
-
/** Mapping between relation and its member representatives */
- std::map< Node, std::vector<Node> > d_membership_db;
+ std::map< Node, std::vector< Node > > d_rReps_memberReps_cache;
- /** Mapping between relation and its members' explanation */
- std::map< Node, std::vector<Node> > d_membership_exp_db;
+ /** Mapping between relation and its member representatives explanation */
+ std::map< Node, std::vector< Node > > d_rReps_memberReps_exp_cache;
/** Mapping between a relation representative and its equivalent relations involving relational operators */
std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache;
- /** Mapping between relation and its member representatives */
- std::map< Node, std::vector<Node> > d_arg_rep_tp_terms;
-
- /** Mapping between TC(r) and one explanation when building TC graph*/
- std::map< Node, Node > d_membership_tc_exp_cache;
-
- /** Mapping between transitive closure relation TC(r) (is not necessary a representative) and members directly asserted members */
- std::map< Node, std::hash_set<Node, NodeHashFunction> > d_tc_membership_db;
-
/** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/
- std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tc_r_graph;
std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_rRep_tcGraph;
std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tcr_tcGraph;
std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
std::map< Node, std::vector< Node > > d_tc_lemmas_last;
- /** Mapping between transitive closure TC(r)'s representative and TC(r) */
std::map< Node, EqcInfo* > d_eqc_info;
public:
void applyTransposeRule( Node rel, Node rel_rep, Node exp );
void applyProductRule( Node rel, Node rel_rep, Node exp );
void applyJoinRule( Node rel, Node rel_rep, Node exp);
+ void applyJoinImageRule( Node mem_rep, Node rel_rep, Node exp);
+ void applyIdenRule( Node mem_rep, Node rel_rep, Node exp);
void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp);
void buildTCGraphForRel( Node tc_rel );
void doTCInference();
void composeMembersForRels( Node );
void computeMembersForBinOpRel( Node );
+ void computeMembersForIdenTerm( Node );
void computeMembersForUnaryOpRel( Node );
+ void computeMembersForJoinImageTerm( Node );
bool isTCReachable( Node mem_rep, Node tc_rel );
void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
void computeTupleReps( Node );
bool areEqual( Node a, Node b );
Node getRepresentative( Node t );
- bool insertIntoIdList(IdList&, int);
bool exists( std::vector<Node>&, Node );
Node mkAnd( std::vector< TNode >& assumptions );
inline void addToMembershipDB( Node, Node, Node );
std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
std::set<Node> newSet;
std::set_union(left.begin(), left.end(), right.begin(), right.end(),
- std::inserter(newSet, newSet.begin()));
+ std::inserter(newSet, newSet.begin()));
Node newNode = NormalForm::elementsToSet(newSet, node.getType());
Assert(newNode.isConst());
Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
std::set<Node>::iterator right_it = right.begin();
int right_len = (*right_it).getType().getTupleLength();
while(right_it != right.end()) {
- Trace("rels-debug") << "Sets::postRewrite processing left_it = " << *right_it << std::endl;
+ Trace("rels-debug") << "Sets::postRewrite processing right_it = " << *right_it << std::endl;
std::vector<Node> right_tuple;
for(int j = 0; j < right_len; j++) {
right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
break;
}
+ case kind::IDEN: {
+ if(node[0].getKind() == kind::EMPTYSET) {
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+ } else if (node[0].isConst()) {
+ std::set<Node> iden_rel_mems;
+ std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]);
+ std::set<Node>::iterator rel_mems_it = rel_mems.begin();
+
+ while( rel_mems_it != rel_mems.end() ) {
+ Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0);
+ iden_rel_mems.insert(RelsUtils::constructPair(node, fst_mem, fst_mem));
+ ++rel_mems_it;
+ }
+
+ Node new_node = NormalForm::elementsToSet(iden_rel_mems, node.getType());
+ Assert(new_node.isConst());
+ Trace("rels-postrewrite") << "Rels::postRewrite returning " << new_node << std::endl;
+ return RewriteResponse(REWRITE_DONE, new_node);
+
+ } else {
+ Trace("rels-postrewrite") << "Rels::postRewrite miss to handle term " << node << std::endl;
+ }
+ break;
+ }
+
+ case kind::JOIN_IMAGE: {
+ unsigned int min_card = node[1].getConst<Rational>().getNumerator().getUnsignedInt();
+ Trace("rels-postrewrite") << "Rels::postRewrite " << node << " with min_card = " << min_card << std::endl;
+
+ if( min_card == 0) {
+ return RewriteResponse(REWRITE_DONE, nm->mkNullaryOperator( node.getType(), kind::UNIVERSE_SET ));
+ } else if(node[0].getKind() == kind::EMPTYSET) {
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+ } else if (node[0].isConst()) {
+ std::set<Node> has_checked;
+ std::set<Node> join_img_mems;
+ std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]);
+ std::set<Node>::iterator rel_mems_it = rel_mems.begin();
+
+ while( rel_mems_it != rel_mems.end() ) {
+ Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0);
+ if( has_checked.find( fst_mem ) != has_checked.end() ) {
+ ++rel_mems_it;
+ continue;
+ }
+ has_checked.insert( fst_mem );
+ std::set<Node> existing_mems;
+ std::set<Node>::iterator rel_mems_it_snd = rel_mems.begin();
+ while( rel_mems_it_snd != rel_mems.end() ) {
+ Node fst_mem_snd = RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 0);
+ if( fst_mem == fst_mem_snd ) {
+ existing_mems.insert( RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 1) );
+ }
+ ++rel_mems_it_snd;
+ }
+ if( existing_mems.size() >= min_card ) {
+ Datatype dt = node.getType().getSetElementType().getDatatype();
+ join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ));
+ }
+ ++rel_mems_it;
+ }
+ Node new_node = NormalForm::elementsToSet(join_img_mems, node.getType());
+ Assert(new_node.isConst());
+ Trace("rels-postrewrite") << "Rels::postRewrite returning " << new_node << std::endl;
+ return RewriteResponse(REWRITE_DONE, new_node);
+ } else {
+ Trace("rels-postrewrite") << "Rels::postRewrite miss to handle term " << node << std::endl;
+ }
+ break;
+ }
+
default:
break;
}//switch(node.getKind())
size_t setNodeIndex = node.getNumChildren()-1;
for(size_t i = 1; i < setNodeIndex; ++i) {
insertedElements = nm->mkNode(kind::UNION,
- insertedElements,
- nm->mkNode(kind::SINGLETON, node[i]));
+ insertedElements,
+ nm->mkNode(kind::SINGLETON, node[i]));
}
return RewriteResponse(REWRITE_AGAIN,
- nm->mkNode(kind::UNION,
- insertedElements,
- node[setNodeIndex]));
+ nm->mkNode(kind::UNION,
+ insertedElements,
+ node[setNodeIndex]));
}//kind::INSERT
else if(node.getKind() == kind::SUBSET) {
TypeNode resultType = firstRelType;
if(!firstRelType.isSet() || !secondRelType.isSet()) {
- throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets");
+ throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-sets");
}
if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
- throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)");
+ throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-relations (sets of tuples)");
}
std::vector<TypeNode> newTupleTypes;
}
};/* struct RelTransClosureTypeRule */
+struct JoinImageTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::JOIN_IMAGE);
+
+ TypeNode firstRelType = n[0].getType(check);
+
+ if(!firstRelType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations");
+ }
+ if(!firstRelType[0].isTuple()) {
+ throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations (sets of tuples)");
+ }
+
+ std::vector<TypeNode> tupleTypes = firstRelType[0].getTupleTypes();
+ if(tupleTypes.size() != 2) {
+ throw TypeCheckingExceptionPrivate(n, " JoinImage operates on a non-binary relation");
+ }
+ TypeNode valType = n[1].getType(check);
+ if (valType != nodeManager->integerType()) {
+ throw TypeCheckingExceptionPrivate(
+ n, " JoinImage cardinality constraint must be integer");
+ }
+ if (n[1].getKind() != kind::CONST_RATIONAL) {
+ throw TypeCheckingExceptionPrivate(
+ n, " JoinImage cardinality constraint must be a constant");
+ }
+ CVC4::Rational r(INT_MAX);
+ if (n[1].getConst<Rational>() > r) {
+ throw TypeCheckingExceptionPrivate(
+ n, " JoinImage Exceeded INT_MAX in cardinality constraint");
+ }
+ if (n[1].getConst<Rational>().getNumerator().getSignedInt() < 0) {
+ throw TypeCheckingExceptionPrivate(
+ n, " JoinImage cardinality constraint must be non-negative");
+ }
+ std::vector<TypeNode> newTupleTypes;
+ newTupleTypes.push_back(tupleTypes[0]);
+ return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
+ }
+
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ Assert(n.getKind() == kind::JOIN_IMAGE);
+ return false;
+ }
+};/* struct JoinImageTypeRule */
+
+struct RelIdenTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::IDEN);
+ TypeNode setType = n[0].getType(check);
+ if(check) {
+ if(!setType.isSet() && !setType.getSetElementType().isTuple()) {
+ throw TypeCheckingExceptionPrivate(n, " Identity operates on non-relation");
+ }
+ if(setType[0].getTupleTypes().size() != 1) {
+ throw TypeCheckingExceptionPrivate(n, " Identity operates on non-unary relations");
+ }
+ }
+ std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
+ tupleTypes.push_back(tupleTypes[0]);
+ return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
+ }
+
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ return false;
+ }
+};/* struct RelIdenTypeRule */
struct SetsProperties {
inline static Cardinality computeCardinality(TypeNode type) {
set-strat.cvc \
rel_tc_8.cvc \
atom_univ2.cvc \
- rels-sharing-simp.cvc
+ rels-sharing-simp.cvc \
+ iden_0.cvc \
+ iden_1_1.cvc \
+ iden_1.cvc \
+ joinImg_0_1.cvc \
+ joinImg_0_2.cvc \
+ joinImg_0.cvc \
+ joinImg_1_1.cvc \
+ joinImg_1.cvc \
+ joinImg_2_1.cvc \
+ joinImg_2.cvc
# unsolved : garbage_collect.cvc
--- /dev/null
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+id : SET OF IntPair;
+
+t : SET OF [INT];
+
+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 TUPLE(1) IS_IN t;
+ASSERT TUPLE(2) IS_IN t;
+ASSERT z IS_IN x;
+ASSERT zt IS_IN x;
+ASSERT v IS_IN x;
+ASSERT a IS_IN x;
+ASSERT id = IDEN(t);
+ASSERT NOT ((1, 1) IS_IN (id & x));
+
+CHECKSAT;
--- /dev/null
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom:TYPE;
+AtomPair: TYPE = [Atom, Atom];
+x : SET OF AtomPair;
+t : SET OF [Atom];
+univ : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+ASSERT univ = UNIVERSE::SET OF [Atom];
+ASSERT (a, b) IS_IN x;
+ASSERT (c, d) IS_IN x;
+ASSERT NOT(a = b);
+ASSERT IDEN(x JOIN univ) = x;
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom:TYPE;
+AtomPair: TYPE = [Atom, Atom];
+x : SET OF AtomPair;
+t : SET OF [Atom];
+univ : SET OF [Atom];
+univ2 : SET OF [Atom,Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+ASSERT univ = UNIVERSE::SET OF [Atom];
+ASSERT univ2 = UNIVERSE::SET OF [Atom, Atom];
+ASSERT univ2 = (univ PRODUCT univ);
+ASSERT (a, b) IS_IN x;
+ASSERT (c, d) IS_IN x;
+ASSERT NOT(a = b);
+ASSERT IDEN(univ) <= x;
+CHECKSAT;
--- /dev/null
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+t : SET OF [INT];
+
+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 z IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+
+ASSERT t = (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT NOT(TUPLE(1) IS_IN (x JOIN_IMAGE 2));
+
+ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(1) IS_IN (x JOIN_IMAGE 1);
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+t : SET OF [INT];
+u : SET OF [INT];
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+b: INT;
+
+ASSERT (1, 7) IS_IN x;
+ASSERT z IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+
+ASSERT t = (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT u = (x JOIN_IMAGE 1);
+
+ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1);
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+t : SET OF [INT];
+u : SET OF [INT];
+univ : SET OF [INT];
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+s : IntPair;
+ASSERT s = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+b: INT;
+
+ASSERT (1, 7) IS_IN x;
+ASSERT z IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+
+ASSERT t = (x JOIN_IMAGE 2);
+ASSERT univ = (x JOIN_IMAGE 0);
+ASSERT TUPLE(100) IS_IN t;
+
+ASSERT NOT (TUPLE(3) IS_IN univ);
+
+ASSERT u = (x JOIN_IMAGE 1);
+
+ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1);
+CHECKSAT;
--- /dev/null
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT x = {(b, c), (d, e), (c, e)};
+ASSERT NOT(a = b);
+
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT t = (x JOIN_IMAGE 2);
+ASSERT x = {(b, c), (d, e), (c, e)};
+ASSERT TUPLE(c) IS_IN t;
+
+CHECKSAT;
--- /dev/null
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+f : Atom;
+g : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 3);
+%ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
+ASSERT x = {(f, g), (b, c), (d, e), (c, e), (f, b)};
+ASSERT (a, f) IS_IN x;
+ASSERT (a, f) IS_IN y;
+ASSERT x = y;
+
+
+
+ASSERT NOT(a = b);
+
+ASSERT NOT (TUPLE(d) IS_IN (x JOIN_IMAGE 2));
+ASSERT f = d;
+
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+f : Atom;
+g : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 1);
+ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
+ASSERT x = {(f, g), (b, c), (d, e), (c, e)};
+ASSERT (NOT(a = b)) OR (NOT(a = f));
+
+CHECKSAT;
\ No newline at end of file
projects / cvc5.git / commitdiff