if(eqc_node[0].isVar()){
reduceTupleVar(eqc_node);
- } else {
- if( safelyAddToMap(d_membership_constraints_cache, rel_rep, tup_rep) ) {
- bool is_true_eq = areEqual(eqc_rep, d_trueNode);
- Node reason = is_true_eq ? eqc_node : eqc_node.negate();
-
- addToMap(d_membership_exp_cache, rel_rep, reason);
- if( is_true_eq ) {
- // add tup_rep to membership database
- // and store mapping between tuple and tuple's elements representatives
- addToMembershipDB(rel_rep, tup_rep, reason);
- }
+ }
+ if( safelyAddToMap(d_membership_constraints_cache, rel_rep, tup_rep) ) {
+ bool is_true_eq = areEqual(eqc_rep, d_trueNode);
+ Node reason = is_true_eq ? eqc_node : eqc_node.negate();
+
+ addToMap(d_membership_exp_cache, rel_rep, reason);
+ if( is_true_eq ) {
+ // add tup_rep to membership database
+ // and store mapping between tuple and tuple's elements representatives
+ addToMembershipDB(rel_rep, tup_rep, reason);
}
}
}
Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 1));
TC_PAIR_IT pair_set_it = tc_graph.find(fst_rep);
+ Trace("rels-tc") << "[sets-rels] **** Member of r = (" << fst_rep << ", " << snd_rep << ")" << std::endl;
+
+ if( pair_set_it != tc_graph.end() ) {
+ pair_set_it->second.insert(snd_rep);
+ } else {
+ std::hash_set< Node, NodeHashFunction > snd_set;
+ snd_set.insert(snd_rep);
+ tc_graph[fst_rep] = snd_set;
+ }
+ }
+ }
+
+ TC_PAIR_IT tc_mem_it = d_tc_membership_db.find(tc_term);
+
+ if( tc_mem_it != d_tc_membership_db.end() ) {
+ for(std::hash_set<Node>::iterator pair_it = tc_mem_it->second.begin();
+ pair_it != tc_mem_it->second.end(); pair_it++) {
+ Node fst_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 0));
+ Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 1));
+ TC_PAIR_IT pair_set_it = tc_graph.find(fst_rep);
+ Trace("rels-tc") << "[sets-rels] **** Member of TC(r) = (" << fst_rep << ", " << snd_rep << ")" << std::endl;
+
if( pair_set_it != tc_graph.end() ) {
pair_set_it->second.insert(snd_rep);
} else {
if(!reason.isNull()) {
d_membership_tc_exp_cache[tc_rep] = reason;
}
- d_membership_tc_cache[tc_rep] = tc_graph;
+ d_tc_graph[tc_rep] = tc_graph;
}
/*
Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSITIVE CLOSURE rule on "
<< tc_term << " with explanation " << exp << std::endl;
- Node tc_rep = getRepresentative(tc_term);
- // build the TC graph for tc_rep if it was not created before
+ Node tc_rep = getRepresentative(tc_term);
+ bool polarity = exp.getKind() != kind::NOT;
+
if( d_rel_nodes.find(tc_rep) == d_rel_nodes.end() ) {
- Trace("rels-debug") << "[sets-rels] Start building the TC graph!" << std::endl;
- Node tc_r_rep = getRepresentative(tc_term[0]);
- constructTCGraph(tc_r_rep, tc_rep, tc_term);
+ d_tc_rep_term[tc_rep] = tc_term;
d_rel_nodes.insert(tc_rep);
}
-
- bool polarity = exp.getKind() != kind::NOT;
-
if(polarity) {
TC_PAIR_IT mem_it = d_tc_membership_db.find(tc_term);
} else {
mem_it->second.insert(exp[0]);
}
+ } else {
+ Trace("rels-tc") << "TC non-member = " << exp << std::endl;
}
//todo: need to construct a tc_graph if transitive closure is used in the context
// // check if tup_rep already exists in TC graph for conflict
void TheorySetsRels::finalizeTCInference() {
- Trace("rels-debug") << "[sets-rels] Finalizing transitive closure inferences!" << std::endl;
+ Trace("rels-tc") << "[sets-rels] ****** Finalizing transitive closure inferences!" << std::endl;
+ std::map<Node, Node>::iterator map_it = d_tc_rep_term.begin();
+
+ while( map_it != d_tc_rep_term.end() ) {
+ Trace("rels-tc") << "[sets-rels] Start building the TC graph for " << map_it->first << std::endl;
- for(TC_IT tc_it = d_membership_tc_cache.begin(); tc_it != d_membership_tc_cache.end(); tc_it++) {
- inferTC(tc_it->first, tc_it->second);
+ constructTCGraph(getRepresentative(map_it->second[0]), map_it->first, map_it->second);
+ inferTC(map_it->first, d_tc_graph[map_it->first]);
+ map_it++;
}
}
void TheorySetsRels::inferTC(Node tc_rep, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph) {
- Trace("rels-debug") << "[sets-rels] Build TC graph for tc_rep = " << tc_rep << std::endl;
+ Trace("rels-tc") << "[sets-rels] Infer TC lemma from tc_graph of " << tc_rep << std::endl;
for(TC_PAIR_IT pair_set_it = tc_graph.begin(); pair_set_it != tc_graph.end(); pair_set_it++) {
for(std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
if(mem_it != d_membership_db.end()) {
if(std::find(mem_it->second.begin(), mem_it->second.end(), pair) == mem_it->second.end()) {
+ Trace("rels-tc") << "[sets-rels] Infered a TC lemma = " << MEMBER(pair, tc_rep) << " by Transitivity"
+ << " with explanation = " << Rewriter::rewrite(exp) << std::endl;
sendLemma( MEMBER(pair, tc_rep), Rewriter::rewrite(exp), "Transitivity" );
}
}
d_rel_nodes.clear();
d_pending_facts.clear();
d_membership_constraints_cache.clear();
- d_membership_tc_cache.clear();
+ d_tc_graph.clear();
d_membership_tc_exp_cache.clear();
d_membership_exp_cache.clear();
d_membership_db.clear();
d_tuple_reps.clear();
d_id_node.clear();
d_node_id.clear();
+ d_tc_rep_term.clear();
}
void TheorySetsRels::doTCLemmas() {
Node tc_rep = getRepresentative(mem_it->first);
Node tc_r_rep = getRepresentative(mem_it->first[0]);
- // build the TC graph for tc_rep if it was not created before
- if( d_rel_nodes.find(tc_rep) == d_rel_nodes.end() ) {
- Trace("rels-debug") << "[sets-rels] Start building the TC graph for relation " << mem_it->first << std::endl;
- constructTCGraph(tc_r_rep, tc_rep, mem_it->first);
- d_rel_nodes.insert(tc_rep);
- }
+// // build the TC graph for tc_rep if it was not created before
+// if( d_rel_nodes.find(tc_rep) == d_rel_nodes.end() ) {
+// Trace("rels-debug") << "[sets-rels] Start building the TC graph for relation " << mem_it->first << std::endl;
+// constructTCGraph(tc_r_rep, tc_rep, mem_it->first);
+// d_rel_nodes.insert(tc_rep);
+// }
std::hash_set< Node, NodeHashFunction >::iterator set_it = mem_it->second.begin();
Node snd = RelsUtils::nthElementOfTuple(*set_it, 1);
Node fst_rep = getRepresentative(fst);
Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(*set_it, 1));
- TC_IT tc_graph_it = d_membership_tc_cache.find(tc_rep);
+ TC_IT tc_graph_it = d_tc_graph.find(tc_rep);
isTCReachable(fst_rep, snd_rep, hasSeen, tc_graph_it->second, isReachable);
- if((tc_graph_it != d_membership_tc_cache.end() && !isReachable) ||
- (tc_graph_it == d_membership_tc_cache.end())) {
+ if((tc_graph_it != d_tc_graph.end() && !isReachable) ||
+ (tc_graph_it == d_tc_graph.end())) {
Node reason = explain(MEMBER(*set_it, mem_it->first));
Node sk_1 = NodeManager::currentNM()->mkSkolem("sde", fst_rep.getType());
Node sk_2 = NodeManager::currentNM()->mkSkolem("sde", snd_rep.getType());
d_infer(c),
d_infer_exp(c),
d_lemma(u),
- d_shared_terms(u),
- d_tc_saver(u)
+ d_shared_terms(u)
{
d_eqEngine->addFunctionKind(kind::PRODUCT);
d_eqEngine->addFunctionKind(kind::JOIN);
Trace("rels-std") << "[sets-rels] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
// Merge membership constraint with "true" or "false" eqc
- // Todo: t1 might not be "true" or "false" rep
if((t1 == d_trueNode || t1 == d_falseNode) &&
t2.getKind() == kind::MEMBER &&
t2[0].getType().isTuple()) {
};
private:
- std::map<int, Node> d_id_node; // mapping between integer id and tuple element rep
- std::map<Node, int> d_node_id; // mapping between tuple element rep and integer id
+ /** Mapping between integer id and tuple element rep */
+ std::map<int, Node> d_id_node;
+
+ /** Mapping between tuple element rep and integer id*/
+ std::map<Node, int> d_node_id;
/** has eqc info */
bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); }
eq::EqualityEngine *d_eqEngine;
context::CDO<bool> *d_conflict;
TheorySets& d_sets_theory;
+
/** True and false constant nodes */
Node d_trueNode;
Node d_falseNode;
- // Facts and lemmas to be sent to EE
+
+ /** Facts and lemmas to be sent to EE */
std::map< Node, Node > d_pending_facts;
std::map< Node, Node > d_pending_split_facts;
std::vector< Node > d_lemma_cache;
NodeList d_pending_merge;
+
/** inferences: maintained to ensure ref count for internally introduced nodes */
NodeList d_infer;
NodeList d_infer_exp;
NodeSet d_lemma;
NodeSet d_shared_terms;
- // tc terms that have been decomposed
- NodeSet d_tc_saver;
+ /** 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;
/** 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) and members directly asserted members */
+ /** 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_membership_tc_cache;
+ std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tc_graph;
+
+ /** Mapping between transitive closure TC(r)'s representative and TC(r) */
+ std::map< Node, Node > d_tc_rep_term;
- /** information necessary for equivalence classes */
public:
void eqNotifyNewClass(Node t);
void eqNotifyPostMerge(Node t1, Node t2);
projects / cvc5.git / commitdiff