Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one " << " node = " << n << std::endl;
std::vector<Node> tuple_elements;
tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor()));
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 0" << std::endl;
for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) {
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 1" << std::endl;
Node element = RelsUtils::nthElementOfTuple(n[0], i);
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 2" << std::endl;
makeSharedTerm(element);
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 3" << std::endl;
tuple_elements.push_back(element);
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 4" << std::endl;
}
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 5" << std::endl;
Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 6" << std::endl;
tuple_reduct = MEMBER(tuple_reduct, n[1]);
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 7" << std::endl;
Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, tuple_reduct);
- Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 8" << std::endl;
sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction");
d_symbolic_tuples.insert(n);
}
eq::EqualityEngine* eq,
context::CDO<bool>* conflict,
TheorySets& d_set ):
+ d_vec_size(c),
d_eqEngine(eq),
d_conflict(conflict),
d_sets_theory(d_set),
}
TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) :
- d_mem(c), d_not_mem(c), d_in(c), d_out(c), d_mem_exp(c),
- d_id_in(c), d_id_out(c), d_tp(c), d_pt(c), d_join(c),d_tc(c) {}
+ d_mem(c), d_not_mem(c), d_mem_exp(c), d_in(c), d_out(c),
+ d_tp(c), d_pt(c), d_join(c), d_tc(c) {}
void TheorySetsRels::eqNotifyNewClass( Node n ) {
Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl;
}
}
- // Create a integer id for tuple element
+ // Create an integer id for tuple element
int TheorySetsRels::getOrMakeElementRepId(EqcInfo* ei, Node e_rep) {
Trace("rels-std") << "[sets-rels] getOrMakeElementRepId:" << " e_rep = " << e_rep << std::endl;
- std::map<Node, int>::iterator nid_it = d_node_id.find(e_rep);
+ std::map< Node, int >::iterator nid_it = d_node_id.find(e_rep);
if( nid_it == d_node_id.end() ) {
- if(d_eqEngine->hasTerm(e_rep)) {
- // it is possible that e's rep changes at this moment, thus we need to know the eqc of e's previous rep
+ if( d_eqEngine->hasTerm(e_rep) ) {
+ // it is possible that e's rep changes at this moment, thus we need to know the previous rep id of eqc of e
eq::EqClassIterator rep_eqc_i = eq::EqClassIterator( e_rep, d_eqEngine );
- while(!rep_eqc_i.isFinished()) {
- std::map<Node, int>::iterator id_it = d_node_id.find(*rep_eqc_i);
+ while( !rep_eqc_i.isFinished() ) {
+ std::map< Node, int >::iterator id_it = d_node_id.find(*rep_eqc_i);
if( id_it != d_node_id.end() ) {
d_id_node[id_it->second] = e_rep;
return true;
}
- void TheorySetsRels::addTCMemAndSendInfer(EqcInfo* tc_ei, Node membership, Node exp, bool fromRel) {
+ void TheorySetsRels::addTCMemAndSendInfer( EqcInfo* tc_ei, Node membership, Node exp, bool fromRel ) {
Trace("rels-std") << "[sets-rels] addTCMemAndSendInfer:" << " membership = " << membership << " from a relation? " << fromRel<< std::endl;
- IdList* in_lst;
- IdList* out_lst;
Node fst = RelsUtils::nthElementOfTuple(membership[0], 0);
Node snd = RelsUtils::nthElementOfTuple(membership[0], 1);
Node fst_rep = getRepresentative(fst);
return;
}
- int fst_rep_id = getOrMakeElementRepId(tc_ei, fst_rep);
- int snd_rep_id = getOrMakeElementRepId(tc_ei, snd_rep);
- IdListMap::iterator tc_in_mem_it = tc_ei->d_id_in.find(snd_rep_id);
-
- if(tc_in_mem_it == tc_ei->d_id_in.end()) {
- in_lst = new(d_sets_theory.getSatContext()->getCMM()) IdList( true, d_sets_theory.getSatContext(), false,
- context::ContextMemoryAllocator<TNode>(d_sets_theory.getSatContext()->getCMM()) );
- tc_ei->d_id_in.insertDataFromContextMemory(snd_rep_id, in_lst);
- Trace("rels-std") << "Create in cache for " << snd_rep << std::endl;
- } else {
- in_lst = (*tc_in_mem_it).second;
- }
+ int fst_rep_id = getOrMakeElementRepId( tc_ei, fst_rep );
+ int snd_rep_id = getOrMakeElementRepId( tc_ei, snd_rep );
std::hash_set<int> in_reachable;
std::hash_set<int> out_reachable;
- collectInReachableNodes(tc_ei, fst_rep_id, in_reachable);
- collectOutReachableNodes(tc_ei, snd_rep_id, out_reachable);
+ collectReachableNodes(tc_ei->d_id_inIds, fst_rep_id, in_reachable);
+ collectReachableNodes(tc_ei->d_id_outIds, snd_rep_id, out_reachable);
// If fst_rep is inserted into in_lst successfully,
// save rep pair's exp and send out TC inference lemmas.
// Otherwise, mem's rep is already in the TC and return.
- if(insertIntoIdList(*in_lst, fst_rep_id)) {
+ if( addId(tc_ei->d_id_inIds, snd_rep_id, fst_rep_id) ) {
Node reason = exp == Node::null() ? explain(membership) : exp;
if(!fromRel && tc_ei->d_tc.get() != membership[1]) {
reason = AND(reason, explain(EQUAL(tc_ei->d_tc.get(), membership[1])));
// Nothing inserted into the eqc
return;
}
-
- IdListMap::iterator tc_out_mem_it = tc_ei->d_id_out.find(fst_rep_id);
- if(tc_out_mem_it == tc_ei->d_id_out.end()) {
- out_lst = new(d_sets_theory.getSatContext()->getCMM()) IdList( true, d_sets_theory.getSatContext(), false,
- context::ContextMemoryAllocator<TNode>(d_sets_theory.getSatContext()->getCMM()) );
- tc_ei->d_id_out.insertDataFromContextMemory(fst_rep_id, out_lst);
- Trace("rels-std") << "Create out arrow cache for " << snd_rep << std::endl;
- } else {
- out_lst = (*tc_out_mem_it).second;
- }
- insertIntoIdList(*out_lst, snd_rep_id);
Trace("rels-std") << "Add out membership arrow for " << fst_rep << " to : " << snd_rep << std::endl;
+ addId(tc_ei->d_id_inIds, fst_rep_id, snd_rep_id);
sendTCInference(tc_ei, in_reachable, out_reachable, mem_rep, fst_rep, snd_rep, fst_rep_id, snd_rep_id);
}
}
}
- void TheorySetsRels::collectInReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& in_reachable, bool firstRound) {
- Trace("rels-std") << "**** Start collecting in-reachable nodes for node with id " << start_id << std::endl;
- if(in_reachable.find(start_id) != in_reachable.end()) {
+ void TheorySetsRels::collectReachableNodes(std::map< int, std::vector< int > >& id_map, int start_id, std::hash_set< int >& reachable_set, bool firstRound) {
+ Trace("rels-std") << "**** Collecting reachable nodes for node with id " << start_id << std::endl;
+ if(reachable_set.find(start_id) != reachable_set.end()) {
return;
}
if(!firstRound) {
- in_reachable.insert(start_id);
+ reachable_set.insert(start_id);
}
- IdListMap::const_iterator id_list_map_it = tc_ei->d_id_in.find(start_id);
- if(id_list_map_it != tc_ei->d_id_in.end()) {
- IdList::const_iterator id_list_it = (*id_list_map_it).second->begin();
- while(id_list_it != (*id_list_map_it).second->end()) {
- collectInReachableNodes(tc_ei, *id_list_it, in_reachable, false);
- id_list_it++;
- }
- }
- }
+ std::vector< int > id_list = getIdList(id_map, start_id);
+ std::vector< int >::iterator id_list_it = id_list.begin();
- void TheorySetsRels::collectOutReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& out_reachable, bool firstRound) {
- Trace("rels-std") << "**** Start collecting out-reachable nodes for node with id " << start_id << std::endl;
- if(out_reachable.find(start_id) != out_reachable.end()) {
- return;
- }
- if(!firstRound) {
- out_reachable.insert(start_id);
- }
- IdListMap::const_iterator id_list_map_it = tc_ei->d_id_out.find(start_id);
-
- if(id_list_map_it != tc_ei->d_id_out.end()) {
- IdList::const_iterator id_list_it = (*id_list_map_it).second->begin();
- while(id_list_it != (*id_list_map_it).second->end()) {
- collectOutReachableNodes(tc_ei, *id_list_it, out_reachable, false);
- id_list_it++;
- }
+ while( id_list_it != id_list.end() ) {
+ collectReachableNodes( id_map, *id_list_it, reachable_set, false );
+ id_list_it++;
}
}
Trace("rels-std") << "[sets-rels] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
// Merge membership constraint with "true" or "false" eqc
- if((t1 == d_trueNode || t1 == d_falseNode) && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple()) {
+ if( (t1 == d_trueNode || t1 == d_falseNode) && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple() ) {
Assert(t1 == d_trueNode || t1 == d_falseNode);
bool polarity = t1 == d_trueNode;
Node t2_1rep = getRepresentative(t2[1]);
EqcInfo* ei = getOrMakeEqcInfo( t2_1rep, true );
- if(polarity) {
+ if( polarity ) {
ei->d_mem.insert(t2[0]);
ei->d_mem_exp[t2[0]] = explain(t2);
} else {
ei->d_not_mem.insert(t2[0]);
}
// Process a membership constraint that a tuple is a member of transpose of rel
- if(!ei->d_tp.get().isNull()) {
+ if( !ei->d_tp.get().isNull() ) {
Node exp = polarity ? explain(t2) : explain(t2.negate());
if(ei->d_tp.get() != t2[1]) {
exp = AND( explain(EQUAL( ei->d_tp.get(), t2[1]) ), exp );
sendInferTranspose( polarity, t2[0], ei->d_tp.get(), exp, true );
}
// Process a membership constraint that a tuple is a member of product of rel
- if(!ei->d_pt.get().isNull()) {
+ if( !ei->d_pt.get().isNull() ) {
Node exp = polarity ? explain(t2) : explain(t2.negate());
if(ei->d_pt.get() != t2[1]) {
exp = AND( explain(EQUAL( ei->d_pt.get(), t2[1]) ), exp );
}
- sendInferProduct(polarity, t2[0], ei->d_pt.get(), exp);
+ sendInferProduct( polarity, t2[0], ei->d_pt.get(), exp );
}
// Process a membership constraint that a tuple is a member of transitive closure of rel
if( polarity && !ei->d_tc.get().isNull() ) {
- addTCMemAndSendInfer(ei, t2, Node::null());
-// Node rel_rep = getRepresentative(ei->d_tc.get()[0]);
-// EqcInfo* rel_ei = getOrMakeEqcInfo(rel_rep);
-// if(rel_ei != NULL) {
-// NodeSet::const_iterator mem = rel_ei->d_mem.begin();
-// while(mem != rel_ei->d_mem.end()) {
-// if(!ei->d_mem.contains(*mem)) {
-// addTCMemAndSendInfer(ei, MEMBER(*mem, rel_rep), rel_ei->d_mem_exp[*mem], true);
-// }
-// mem++;
-// }
-// }
+ addTCMemAndSendInfer( ei, t2, Node::null() );
}
// Merge two relation eqcs
- } else if(t1.getType().isSet() &&
- t2.getType().isSet() &&
- t1.getType().getSetElementType().isTuple()) {
+ } else if( t1.getType().isSet() && t2.getType().isSet() && t1.getType().getSetElementType().isTuple() ) {
mergeTransposeEqcs(t1, t2);
mergeProductEqcs(t1, t2);
mergeTCEqcs(t1, t2);
NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin();
while(t1_mem_it != t1_ei->d_mem.end()) {
- Node membership = MEMBER(*t1_mem_it, t1_ei->d_tc.get());
NodeMap::const_iterator reason_it = t1_ei->d_mem_exp.find(*t1_mem_it);
Assert(reason_it != t1_ei->d_mem_exp.end());
- addTCMemAndSendInfer(t1_ei, membership, (*reason_it).second);
+ addTCMemAndSendInfer(t1_ei, MEMBER(*t1_mem_it, t1_ei->d_tc.get()), (*reason_it).second);
t1_mem_it++;
}
}
}
+ bool TheorySetsRels::addId( std::map< int, std::vector< int > >& id_map, int key, int id ) {
+ int n_data = d_vec_size[key];
+ int len = n_data < id_map[key].size() ? n_data : id_map[key].size();
+
+ for( int i = 0; i < len; i++ ) {
+ if( id_map[key][i] == id) {
+ return false;
+ }
+ }
+ if( n_data < id_map[key].size() ) {
+ id_map[key][n_data] = id;
+ } else {
+ id_map[key].push_back( id );
+ }
+ d_vec_size[key] = n_data+1;
+ return true;
+ }
+
+ std::vector< int > TheorySetsRels::getIdList( std::map< int, std::vector< int > >& id_map, int key ) {
+ std::vector< int > id_list;
+ int n_data = d_vec_size[key];
+ int len = n_data < id_map[key].size() ? n_data : id_map[key].size();
+
+ for( int i = 0; i < len; i++ ) {
+ id_list.push_back(id_map[key][i]);
+ }
+ return id_list;
+ }
+
}
}
}
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;
+ 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:
TheorySetsRels(context::Context* c,
static int counter;
NodeSet d_mem;
NodeSet d_not_mem;
+ NodeMap d_mem_exp;
NodeListMap d_in;
NodeListMap d_out;
- NodeMap d_mem_exp;
- IdListMap d_id_in; // mapping from a element rep id to a list of rep ids that pointed by
- IdListMap d_id_out; // mapping from a element rep id to a list of rep ids that point to
context::CDO< Node > d_tp;
context::CDO< Node > d_pt;
context::CDO< Node > d_join;
context::CDO< Node > d_tc;
+ /** mapping from an element rep id to a list of rep ids that pointed by */
+ /** Context dependent map Int -> IntList */
+ std::map< int, std::vector< int > > d_id_inIds;
+ /** mapping from an element rep id to a list of rep ids that point to */
+ /** Context dependent map Int -> IntList */
+ std::map< int, std::vector< int > > d_id_outIds;
};
private:
+ /** Context */
+ context::CDHashMap< int, int > d_vec_size;
+
/** Mapping between integer id and tuple element rep */
- std::map<int, Node> d_id_node;
+ std::map< int, Node > d_id_node;
/** Mapping between tuple element rep and integer id*/
- std::map<Node, int> d_node_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(); }
+ bool addId( std::map< int, std::vector< int > >& id_map, int key, int id );
+ std::vector< int > getIdList( std::map< int, std::vector< int > >& id_map, int key );
+
+ void collectReachableNodes(std::map< int, std::vector< int > >& id_map, int start_id, std::hash_set<int>& reachable_set, bool firstRound=true);
+
private:
eq::EqualityEngine *d_eqEngine;
EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false );
void sendInferTranspose(bool, Node, Node, Node, bool reverseOnly = false);
void addTCMemAndSendInfer(EqcInfo* tc_ei, Node mem, Node exp, bool fromRel = false);
- void collectInReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& in_reachable, bool firstRound = true);
- void collectOutReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& out_reachable, bool firstRound = true);
void sendTCInference(EqcInfo* tc_ei, std::hash_set<int> in_reachable, std::hash_set<int> out_reachable, Node mem_rep, Node fst_rep, Node snd_rep, int id1, int id2);
projects / cvc5.git / commitdiff