From: Andrew Reynolds Date: Mon, 8 Jul 2019 22:16:50 +0000 (-0500) Subject: Towards refactoring relations (#3078) X-Git-Tag: cvc5-1.0.0~4093 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=77db9e59b783667149c2a71b730e26fe74084073;p=cvc5.git Towards refactoring relations (#3078) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index cc13dec6d..058e848d6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -614,6 +614,8 @@ libcvc4_add_sources( theory/sep/theory_sep_type_rules.h theory/sets/normal_form.h theory/sets/rels_utils.h + theory/sets/skolem_cache.cpp + theory/sets/skolem_cache.h theory/sets/theory_sets.cpp theory/sets/theory_sets.h theory/sets/theory_sets_private.cpp diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml index 3d46b3be3..766da793a 100644 --- a/src/options/sets_options.toml +++ b/src/options/sets_options.toml @@ -20,15 +20,6 @@ header = "options/sets_options.h" read_only = true help = "send inferences as lemmas" -[[option]] - name = "setsRelEager" - category = "regular" - long = "sets-rel-eager" - type = "bool" - default = "true" - read_only = true - help = "standard effort checks for relations" - [[option]] name = "setsExt" category = "regular" diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp new file mode 100644 index 000000000..99e6588ca --- /dev/null +++ b/src/theory/sets/skolem_cache.cpp @@ -0,0 +1,57 @@ +/********************* */ +/*! \file skolem_cache.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of a cache of skolems for theory of sets. + **/ + +#include "theory/sets/skolem_cache.h" + +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace sets { + +SkolemCache::SkolemCache() {} + +Node SkolemCache::mkTypedSkolemCached( + TypeNode tn, Node a, Node b, SkolemId id, const char* c) +{ + a = a.isNull() ? a : Rewriter::rewrite(a); + b = b.isNull() ? b : Rewriter::rewrite(b); + + std::map::iterator it = d_skolemCache[a][b].find(id); + if (it == d_skolemCache[a][b].end()) + { + Node sk = mkTypedSkolem(tn, c); + d_skolemCache[a][b][id] = sk; + return sk; + } + return it->second; +} + +Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c) +{ + Node n = NodeManager::currentNM()->mkSkolem(c, tn, "sets skolem"); + d_allSkolems.insert(n); + return n; +} + +bool SkolemCache::isSkolem(Node n) const +{ + return d_allSkolems.find(n) != d_allSkolems.end(); +} + +} // namespace sets +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h new file mode 100644 index 000000000..74a8073d4 --- /dev/null +++ b/src/theory/sets/skolem_cache.h @@ -0,0 +1,73 @@ +/********************* */ +/*! \file skolem_cache.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A cache of skolems for theory of sets. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__SETS__SKOLEM_CACHE_H +#define CVC4__THEORY__SETS__SKOLEM_CACHE_H + +#include +#include + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace sets { + +/** + * A cache of all set skolems generated by the TheorySets class. This + * cache is used to ensure that duplicate skolems are not generated when + * possible, and helps identify what skolems were allocated in the current run. + */ +class SkolemCache +{ + public: + SkolemCache(); + /** Identifiers for skolem types + * + * The comments below document the properties of each skolem introduced by + * inference in the sets solver, where by skolem we mean the fresh + * set variable that witnesses each of "exists k". + */ + enum SkolemId + { + // (a,b) in join(A,B) => exists k. (a,k) in A ^ (k,b) in B + // This is cached by the nodes corresponding to (a,b) and join(A,B). + SK_JOIN, + }; + + /** + * Makes a skolem of type tn that is cached based on the key (a,b,id). + * Argument c is the variable name of the skolem. + */ + Node mkTypedSkolemCached( + TypeNode tn, Node a, Node b, SkolemId id, const char* c); + /** Same as above, but without caching. */ + Node mkTypedSkolem(TypeNode tn, const char* c); + /** Returns true if n is a skolem allocated by this class */ + bool isSkolem(Node n) const; + + private: + /** map from node pairs and identifiers to skolems */ + std::map > > d_skolemCache; + /** the set of all skolems we have generated */ + std::unordered_set d_allSkolems; +}; + +} // namespace sets +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index a62a235c3..6e71ab2ad 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -26,9 +26,8 @@ #include "theory/theory_model.h" #include "util/result.h" -#define AJR_IMPLEMENTATION - using namespace std; +using namespace CVC4::kind; namespace CVC4 { namespace theory { @@ -54,8 +53,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_notify(*this), d_equalityEngine(d_notify, c, "theory::sets::ee", true), d_conflict(c), - d_rels( - new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external)), + d_rels(new TheorySetsRels(c, u, &d_equalityEngine, *this)), d_rels_enabled(false) { d_true = NodeManager::currentNM()->mkConst( true ); @@ -84,9 +82,6 @@ void TheorySetsPrivate::eqNotifyNewClass(TNode t) { EqcInfo * e = getOrMakeEqcInfo( t, true ); e->d_singleton = t; } - if( options::setsRelEager() ){ - d_rels->eqNotifyNewClass( t ); - } } void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){ @@ -179,9 +174,6 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){ } d_members[t1] = n_members; } - if( options::setsRelEager() ){ - d_rels->eqNotifyPostMerge( t1, t2 ); - } } } @@ -535,11 +527,13 @@ void TheorySetsPrivate::fullEffortCheck(){ std::vector< Node > lemmas; Trace("sets-eqc") << "Equality Engine:" << std::endl; + std::map eqcTypeCount; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); bool isSet = false; TypeNode tn = eqc.getType(); + eqcTypeCount[tn]++; //common type node and term TypeNode tnc; Node tnct; @@ -667,7 +661,17 @@ void TheorySetsPrivate::fullEffortCheck(){ Trace("sets-eqc") << std::endl; ++eqcs_i; } - + + if (Trace.isOn("sets-state")) + { + Trace("sets-state") << "Equivalence class counters:" << std::endl; + for (std::pair& ec : eqcTypeCount) + { + Trace("sets-state") + << " " << ec.first << " -> " << ec.second << std::endl; + } + } + flushLemmas( lemmas ); if( !hasProcessed() ){ if( Trace.isOn("sets-mem") ){ @@ -736,6 +740,11 @@ void TheorySetsPrivate::fullEffortCheck(){ } } } + if (!hasProcessed()) + { + // invoke relations solver + d_rels->check(Theory::EFFORT_FULL); + } }while( !d_sentLemma && !d_conflict && d_addedFact ); Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl; } @@ -1755,19 +1764,11 @@ void TheorySetsPrivate::check(Theory::Effort level) { if( level == Theory::EFFORT_FULL ){ if( !d_external.d_valuation.needCheck() ){ fullEffortCheck(); - if( !d_conflict && !d_sentLemma ){ - //invoke relations solver - d_rels->check(level); - } if (!d_conflict && !d_sentLemma && d_full_check_incomplete) { d_external.d_out->setIncomplete(); } } - }else{ - if( options::setsRelEager() ){ - d_rels->check(level); - } } } Trace("sets-check") << "Sets finish Check effort " << level << std::endl; @@ -1888,8 +1889,8 @@ void TheorySetsPrivate::computeCareGraph() { //populate indices for( unsigned i=0; isecond.size(); i++ ){ TNode f1 = it->second[i]; - Assert(d_equalityEngine.hasTerm(f1)); Trace("sets-cg-debug") << "...build for " << f1 << std::endl; + Assert(d_equalityEngine.hasTerm(f1)); //break into index based on operator, and type of first argument (since some operators are parametric) TypeNode tn = f1[0].getType(); std::vector< TNode > reps; @@ -2146,6 +2147,30 @@ bool TheorySetsPrivate::propagate(TNode literal) { return ok; }/* TheorySetsPrivate::propagate(TNode) */ +void TheorySetsPrivate::processInference(Node lem, + const char* c, + std::vector& lemmas) +{ + Trace("sets-pinfer") << "Process inference: " << lem << std::endl; + if (lem.getKind() != IMPLIES || !isEntailed(lem[0], true)) + { + Trace("sets-pinfer") << " must assert as lemma" << std::endl; + lemmas.push_back(lem); + return; + } + // try to assert it as a fact + Trace("sets-pinfer") << "Process conclusion: " << lem[1] << std::endl; + Trace("sets-pinfer") << " assert as fact" << std::endl; + assertInference(lem[1], lem[0], lemmas, c); +} + +bool TheorySetsPrivate::isInConflict() const { return d_conflict.get(); } +bool TheorySetsPrivate::sentLemma() const { return d_sentLemma; } + +OutputChannel* TheorySetsPrivate::getOutputChannel() +{ + return d_external.d_out; +} void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 3014b2f2a..cb3189e81 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -22,6 +22,7 @@ #include "context/cdhashset.h" #include "context/cdqueue.h" #include "expr/node_trie.h" +#include "theory/sets/skolem_cache.h" #include "theory/sets/theory_sets_rels.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -69,9 +70,7 @@ private: void checkDisequalities( std::vector< Node >& lemmas ); bool isMember( Node x, Node s ); bool isSetDisequalityEntailed( Node s, Node t ); - - void flushLemmas( std::vector< Node >& lemmas, bool preprocess = false ); - void flushLemma( Node lem, bool preprocess = false ); + Node getProxy( Node n ); Node getCongruent( Node n ); Node getEmptySet( TypeNode tn ); @@ -222,6 +221,12 @@ private: //for universe set EqualityStatus getEqualityStatus(TNode a, TNode b); + /** + * Get the skolem cache of this theory, which manages a database of introduced + * skolem variables used for various inferences. + */ + SkolemCache& getSkolemCache() { return d_skCache; } + void preRegisterTerm(TNode node); /** expandDefinition @@ -262,7 +267,38 @@ private: //for universe set void propagate(Theory::Effort); -private: + /** Process inference + * + * Argument lem specifies an inference inferred by this theory. If lem is + * an IMPLIES node, then its antecendant is the explanation of the conclusion. + * + * Argument c is used for debugging, typically the name of the inference. + * + * This method may add facts to the equality engine of theory of sets. + * Any (portion of) the conclusion of lem that is not sent to the equality + * engine is added to the argument lemmas, which should be processed via the + * caller of this method. + */ + void processInference(Node lem, const char* c, std::vector& lemmas); + /** Flush lemmas + * + * This sends lemmas on the output channel of the theory of sets. + * + * The argument preprocess indicates whether preprocessing should be applied + * (by TheoryEngine) on each of lemmas. + */ + void flushLemmas(std::vector& lemmas, bool preprocess = false); + /** singular version of above */ + void flushLemma(Node lem, bool preprocess = false); + /** Are we currently in conflict? */ + bool isInConflict() const; + /** Have we sent out a lemma during a call to a full effort check? */ + bool sentLemma() const; + + /** get default output channel */ + OutputChannel* getOutputChannel(); + + private: TheorySets& d_external; class Statistics { @@ -321,6 +357,8 @@ public: private: /** subtheory solver for the theory of relations */ std::unique_ptr d_rels; + /** the skolem cache */ + SkolemCache d_skCache; /** are relations enabled? * * This flag is set to true during a full effort check if any constraint diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 74d0e5bd8..2bbaa3bc8 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -20,6 +20,7 @@ #include "theory/sets/theory_sets.h" using namespace std; +using namespace CVC4::kind; namespace CVC4 { namespace theory { @@ -31,19 +32,45 @@ typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT; - void TheorySetsRels::check(Theory::Effort level) { - Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl; - if(Theory::fullEffort(level)) { - collectRelsInfo(); - check(); - doPendingLemmas(); - Assert( d_lemmas_out.empty() ); - Assert( d_pending_facts.empty() ); - } else { - doPendingMerge(); - } - Trace("rels") << "\n[sets-rels] ******************************* Done with the relational solver *******************************\n" << std::endl; +TheorySetsRels::TheorySetsRels(context::Context* c, + context::UserContext* u, + eq::EqualityEngine* eq, + TheorySetsPrivate& set) + : d_eqEngine(eq), + d_sets_theory(set), + d_trueNode(NodeManager::currentNM()->mkConst(true)), + d_falseNode(NodeManager::currentNM()->mkConst(false)), + d_shared_terms(u), + d_satContext(c) +{ + d_eqEngine->addFunctionKind(PRODUCT); + d_eqEngine->addFunctionKind(JOIN); + d_eqEngine->addFunctionKind(TRANSPOSE); + d_eqEngine->addFunctionKind(TCLOSURE); + d_eqEngine->addFunctionKind(JOIN_IMAGE); + d_eqEngine->addFunctionKind(IDEN); + d_eqEngine->addFunctionKind(APPLY_CONSTRUCTOR); +} + +TheorySetsRels::~TheorySetsRels() {} + +void TheorySetsRels::check(Theory::Effort level) +{ + Trace("rels") << "\n[sets-rels] ******************************* Start the " + "relational solver, effort = " + << level << " *******************************\n" + << std::endl; + if (Theory::fullEffort(level)) + { + collectRelsInfo(); + check(); + doPendingInfers(); } + Assert(d_pending.empty()); + Trace("rels") << "\n[sets-rels] ******************************* Done with " + "the relational solver *******************************\n" + << std::endl; +} void TheorySetsRels::check() { MEM_IT m_it = d_rReps_memberReps_cache.begin(); @@ -54,41 +81,42 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti for(unsigned int i = 0; i < m_it->second.size(); i++) { Node mem = d_rReps_memberReps_cache[rel_rep][i]; Node exp = d_rReps_memberReps_exp_cache[rel_rep][i]; - std::map > kind_terms = d_terms_cache[rel_rep]; + std::map >& kind_terms = + d_terms_cache[rel_rep]; if( kind_terms.find(kind::TRANSPOSE) != kind_terms.end() ) { - std::vector tp_terms = kind_terms[kind::TRANSPOSE]; + std::vector& tp_terms = kind_terms[TRANSPOSE]; 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 join_terms = kind_terms[kind::JOIN]; + std::vector& join_terms = kind_terms[JOIN]; for( unsigned int j = 0; j < join_terms.size(); j++ ) { applyJoinRule( join_terms[j], rel_rep, exp ); } } if( kind_terms.find(kind::PRODUCT) != kind_terms.end() ) { - std::vector product_terms = kind_terms[kind::PRODUCT]; + std::vector& product_terms = kind_terms[PRODUCT]; for( unsigned int j = 0; j < product_terms.size(); j++ ) { applyProductRule( product_terms[j], rel_rep, exp ); } } if( kind_terms.find(kind::TCLOSURE) != kind_terms.end() ) { - std::vector tc_terms = kind_terms[kind::TCLOSURE]; + std::vector& tc_terms = kind_terms[TCLOSURE]; for( unsigned int j = 0; j < tc_terms.size(); j++ ) { applyTCRule( mem, tc_terms[j], rel_rep, exp ); } } if( kind_terms.find(kind::JOIN_IMAGE) != kind_terms.end() ) { - std::vector join_image_terms = kind_terms[kind::JOIN_IMAGE]; + std::vector& join_image_terms = kind_terms[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 iden_terms = kind_terms[kind::IDEN]; + std::vector& iden_terms = kind_terms[IDEN]; for( unsigned int j = 0; j < iden_terms.size(); j++ ) { applyIdenRule( mem, iden_terms[j], exp ); } @@ -141,6 +169,17 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti t_it++; } doTCInference(); + + // clean up + d_tuple_reps.clear(); + d_rReps_memberReps_exp_cache.clear(); + d_terms_cache.clear(); + d_membership_trie.clear(); + d_rel_nodes.clear(); + d_rReps_memberReps_cache.clear(); + d_rRep_tcGraph.clear(); + d_tcr_tcGraph_exps.clear(); + d_tcr_tcGraph.clear(); } /* @@ -154,6 +193,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti Node eqc_rep = (*eqcs_i); eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine ); + TypeNode erType = eqc_rep.getType(); Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl; while( !eqc_i.isFinished() ){ @@ -161,9 +201,8 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti Trace("rels-ee") << " term : " << eqc_node << std::endl; - if( getRepresentative(eqc_rep) == getRepresentative(d_trueNode) || - getRepresentative(eqc_rep) == getRepresentative(d_falseNode) ) { - + if (erType.isBoolean() && eqc_rep.isConst()) + { // collect membership info if( eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple()) { Node tup_rep = getRepresentative( eqc_node[0] ); @@ -173,19 +212,21 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti reduceTupleVar( eqc_node ); } - bool is_true_eq = areEqual( eqc_rep, d_trueNode ); + bool is_true_eq = eqc_rep.getConst(); Node reason = is_true_eq ? eqc_node : eqc_node.negate(); if( is_true_eq ) { if( safelyAddToMap(d_rReps_memberReps_cache, rel_rep, tup_rep) ) { - addToMap(d_rReps_memberReps_exp_cache, rel_rep, reason); + d_rReps_memberReps_exp_cache[rel_rep].push_back(reason); computeTupleReps(tup_rep); d_membership_trie[rel_rep].addTerm(tup_rep, d_tuple_reps[tup_rep]); } } } // collect relational terms info - } else if( eqc_rep.getType().isSet() && eqc_rep.getType().getSetElementType().isTuple() ) { + } + else if (erType.isSet() && erType.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::JOIN_IMAGE || eqc_node.getKind() == kind::IDEN ) { @@ -209,8 +250,11 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti } } // need to add all tuple elements as shared terms - } else if( eqc_node.getType().isTuple() && !eqc_node.isConst() && !eqc_node.isVar() ) { - for( unsigned int i = 0; i < eqc_node.getType().getTupleLength(); i++ ) { + } + else if (erType.isTuple() && !eqc_node.isConst() && !eqc_node.isVar()) + { + for (unsigned i = 0, tlen = erType.getTupleLength(); i < tlen; i++) + { Node element = RelsUtils::nthElementOfTuple( eqc_node, i ); if( !element.isConst() ) { @@ -238,6 +282,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti if( rel_mem_it == d_rReps_memberReps_cache.end() ) { return; } + NodeManager* nm = NodeManager::currentNM(); Node join_image_rel = join_image_term[0]; std::unordered_set< Node, NodeHashFunction > hasChecked; @@ -262,7 +307,8 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ), join_image_term); - if( holds( new_membership ) ) { + if (d_sets_theory.isEntailed(new_membership, true)) + { ++mem_rep_it; ++mem_rep_exp_it; continue; @@ -302,7 +348,10 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti 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" ); + sendInfer( + new_membership, + reasons.size() > 1 ? nm->mkNode(AND, reasons) : reasons[0], + "JOIN-IMAGE UP"); break; } } @@ -359,7 +408,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti 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" ); + sendInfer(conclusion, reason, "JOIN-IMAGE DOWN"); Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl; } @@ -374,6 +423,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti 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; + NodeManager* nm = NodeManager::currentNM(); if( d_rel_nodes.find( iden_term ) == d_rel_nodes.end() ) { computeMembersForIdenTerm( iden_term ); d_rel_nodes.insert( iden_term ); @@ -387,7 +437,9 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti 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" ); + sendInfer(nm->mkNode(AND, fact, nm->mkNode(EQUAL, fst_mem, snd_mem)), + reason, + "IDENTITY-DOWN"); Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyIdenRule on " << iden_term << std::endl; } @@ -405,6 +457,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti if( d_rReps_memberReps_cache.find( iden_term_rel_rep ) == d_rReps_memberReps_cache.end() ) { return; } + NodeManager* nm = NodeManager::currentNM(); 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(); @@ -417,7 +470,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti 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" ); + sendInfer(nm->mkNode(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; @@ -513,10 +566,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti (NodeManager::currentNM()->mkNode(kind::OR, sk_eq, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_1, sk_2), tc_rel)))))))); Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, conclusion ); - std::vector< Node > require_phase; - require_phase.push_back(Rewriter::rewrite(mem_of_r)); - require_phase.push_back(Rewriter::rewrite(sk_eq)); - d_tc_lemmas_last[tc_lemma] = require_phase; + d_pending.push_back(tc_lemma); } bool TheorySetsRels::isTCReachable( Node mem_rep, Node tc_rel ) { @@ -617,6 +667,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) { + NodeManager* nm = NodeManager::currentNM(); Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) ); std::vector< Node > all_reasons( reasons ); @@ -634,9 +685,13 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel[0], reasons.back()[1]) ); } if( all_reasons.size() > 1) { - sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tc_mem, tc_rel), NodeManager::currentNM()->mkNode(kind::AND, all_reasons), "TCLOSURE-Forward"); + sendInfer(nm->mkNode(MEMBER, tc_mem, tc_rel), + nm->mkNode(AND, all_reasons), + "TCLOSURE-Forward"); } else { - sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tc_mem, tc_rel), all_reasons.front(), "TCLOSURE-Forward"); + sendInfer(nm->mkNode(MEMBER, tc_mem, tc_rel), + all_reasons.front(), + "TCLOSURE-Forward"); } // check if cur_node has been traversed or not @@ -706,8 +761,8 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti if( pt_rel != exp[1] ) { reason = NodeManager::currentNM()->mkNode(kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, pt_rel, exp[1])); } - sendInfer( fact_1, reason, "product-split" ); - sendInfer( fact_2, reason, "product-split" ); + sendInfer(fact_1, reason, "product-split"); + sendInfer(fact_2, reason, "product-split"); } /* join-split rule: (a, b) IS_IN (X JOIN Y) @@ -738,7 +793,8 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti Node r1_rep = getRepresentative(join_rel[0]); Node r2_rep = getRepresentative(join_rel[1]); TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0]; - Node shared_x = NodeManager::currentNM()->mkSkolem("srj_", shared_type); + Node shared_x = d_sets_theory.getSkolemCache().mkTypedSkolemCached( + shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj"); Datatype dt = join_rel[0].getType().getSetElementType().getDatatype(); unsigned int s1_len = join_rel[0].getType().getSetElementType().getTupleLength(); unsigned int tup_len = join_rel.getType().getSetElementType().getTupleLength(); @@ -776,9 +832,9 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, join_rel, exp[1])); } Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, join_rel[0]); - sendInfer( fact, reason, "JOIN-Split" ); + sendInfer(fact, reason, "JOIN-Split-1"); fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]); - sendInfer( fact, reason, "JOIN-Split" ); + sendInfer(fact, reason, "JOIN-Split-2"); makeSharedTerm( shared_x ); } @@ -796,9 +852,12 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti if( tp_terms.size() < 1) { return; } + NodeManager* nm = NodeManager::currentNM(); for( unsigned int i = 1; i < tp_terms.size(); i++ ) { Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE-Equal rule on transposed term = " << tp_terms[0] << " and " << tp_terms[i] << std::endl; - sendInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, tp_terms[0][0], tp_terms[i][0]), NodeManager::currentNM()->mkNode(kind::EQUAL, tp_terms[0], tp_terms[i]), "TRANSPOSE-Equal"); + sendInfer(nm->mkNode(EQUAL, tp_terms[0][0], tp_terms[i][0]), + nm->mkNode(EQUAL, tp_terms[0], tp_terms[i]), + "TRANSPOSE-Equal"); } } @@ -806,6 +865,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE rule on transposed term = " << tp_rel << ", its representative = " << tp_rel_rep << " with explanation = " << exp << std::endl; + NodeManager* nm = NodeManager::currentNM(); if(d_rel_nodes.find( tp_rel ) == d_rel_nodes.end()) { Trace("rels-debug") << "\n[Theory::Rels] Apply TRANSPOSE-Compose rule on term: " << tp_rel @@ -821,7 +881,9 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti if( tp_rel != exp[1] ) { reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tp_rel, exp[1])); } - sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, reversed_mem, tp_rel[0]), reason, "TRANSPOSE-Reverse" ); + sendInfer(nm->mkNode(MEMBER, reversed_mem, tp_rel[0]), + reason, + "TRANSPOSE-Reverse"); } void TheorySetsRels::doTCInference() { @@ -892,8 +954,12 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti } Node rel0_rep = getRepresentative(rel[0]); - if(d_rReps_memberReps_cache.find( rel0_rep ) == d_rReps_memberReps_cache.end()) + if (d_rReps_memberReps_cache.find(rel0_rep) + == d_rReps_memberReps_cache.end()) + { return; + } + NodeManager* nm = NodeManager::currentNM(); std::vector members = d_rReps_memberReps_cache[rel0_rep]; std::vector exps = d_rReps_memberReps_exp_cache[rel0_rep]; @@ -906,7 +972,9 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti if( rel[0] != exps[i][1] ) { reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, rel[0], exps[i][1])); } - sendInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel), reason, "TRANSPOSE-reverse"); + sendInfer(nm->mkNode(MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel), + reason, + "TRANSPOSE-reverse"); } } } @@ -927,6 +995,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti d_rReps_memberReps_cache.find( r2_rep ) == d_rReps_memberReps_cache.end() ) { return; } + NodeManager* nm = NodeManager::currentNM(); std::vector r1_rep_exps = d_rReps_memberReps_exp_cache[r1_rep]; std::vector r2_rep_exps = d_rReps_memberReps_exp_cache[r2_rep]; @@ -971,12 +1040,14 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1]) ); } if( isProduct ) { - sendInfer( fact, NodeManager::currentNM()->mkNode(kind::AND, reasons), "PRODUCT-Compose" ); + sendInfer(fact, + nm->mkNode(kind::AND, reasons), + "PRODUCT-Compose"); } else { if( r1_rmost != r2_lmost ) { reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1_rmost, r2_lmost) ); } - sendInfer( fact, NodeManager::currentNM()->mkNode(kind::AND, reasons), "JOIN-Compose" ); + sendInfer(fact, nm->mkNode(kind::AND, reasons), "JOIN-Compose"); } } } @@ -984,104 +1055,33 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti } - void TheorySetsRels::doPendingLemmas() { - Trace("rels-debug") << "[Theory::Rels] **************** Start doPendingLemmas !" << std::endl; - if( !(*d_conflict) ){ - if ( (!d_lemmas_out.empty() || !d_pending_facts.empty()) ) { - for( unsigned i=0; i < d_lemmas_out.size(); i++ ){ - Assert(d_lemmas_out[i].getKind() == kind::IMPLIES); - if(holds( d_lemmas_out[i][1] )) { - Trace("rels-lemma-skip") << "[sets-rels-lemma-skip] Skip an already held lemma: " - << d_lemmas_out[i]<< std::endl; - continue; - } - d_sets_theory.d_out->lemma( d_lemmas_out[i] ); - Trace("rels-lemma") << "[sets-rels-lemma] Send out a lemma : " - << d_lemmas_out[i] << std::endl; - } - for( std::map::iterator pending_it = d_pending_facts.begin(); - pending_it != d_pending_facts.end(); pending_it++ ) { - if( holds( pending_it->first ) ) { - Trace("rels-lemma-skip") << "[sets-rels-fact-lemma-skip] Skip an already held fact,: " - << pending_it->first << std::endl; - continue; - } - Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, pending_it->second, pending_it->first); - if( d_lemmas_produced.find( lemma ) == d_lemmas_produced.end() ) { - d_sets_theory.d_out->lemma(NodeManager::currentNM()->mkNode(kind::IMPLIES, pending_it->second, pending_it->first)); - Trace("rels-lemma") << "[sets-rels-fact-lemma] Send out a fact as lemma : " - << pending_it->first << " with reason " << pending_it->second << std::endl; - d_lemmas_produced.insert( lemma ); - } + void TheorySetsRels::doPendingInfers() + { + // process the inferences in d_pending + if (!d_sets_theory.isInConflict()) + { + std::vector lemmas; + for (const Node& p : d_pending) + { + d_sets_theory.processInference(p, "rels", lemmas); + if (d_sets_theory.isInConflict()) + { + break; } } + // if we are still not in conflict, send lemmas + if (!d_sets_theory.isInConflict()) + { + d_sets_theory.flushLemmas(lemmas); + } } - doTCLemmas(); - Trace("rels-debug") << "[Theory::Rels] **************** Done with doPendingLemmas !" << std::endl; - d_tuple_reps.clear(); - d_rReps_memberReps_exp_cache.clear(); - d_terms_cache.clear(); - d_lemmas_out.clear(); - d_membership_trie.clear(); - d_rel_nodes.clear(); - d_pending_facts.clear(); - d_rReps_memberReps_cache.clear(); - d_rRep_tcGraph.clear(); - d_tcr_tcGraph_exps.clear(); - d_tcr_tcGraph.clear(); - d_tc_lemmas_last.clear(); + d_pending.clear(); } - bool TheorySetsRels::isRelationKind( Kind k ) { return k == kind::TRANSPOSE || k == kind::PRODUCT || k == kind::JOIN || k == kind::TCLOSURE; } - void TheorySetsRels::doTCLemmas() { - Trace("rels-debug") << "[Theory::Rels] **************** Start doTCLemmas !" << std::endl; - std::map< Node, std::vector< Node > >::iterator tc_lemma_it = d_tc_lemmas_last.begin(); - while( tc_lemma_it != d_tc_lemmas_last.end() ) { - if( !holds( tc_lemma_it->first[1] ) ) { - if( d_lemmas_produced.find( tc_lemma_it->first ) == d_lemmas_produced.end() ) { - d_sets_theory.d_out->lemma( tc_lemma_it->first ); - d_lemmas_produced.insert( tc_lemma_it->first ); - - for( unsigned int i = 0; i < (tc_lemma_it->second).size(); i++ ) { - if( (tc_lemma_it->second)[i] == d_falseNode ) { - d_sets_theory.d_out->requirePhase((tc_lemma_it->second)[i], true); - } - } - Trace("rels-lemma") << "[Theory::Rels] **** Send out a TC lemma = " << tc_lemma_it->first << " by " << "TCLOSURE-Forward"<< std::endl; - } - } - ++tc_lemma_it; - } - Trace("rels-debug") << "[Theory::Rels] **************** Done with doTCLemmas !" << std::endl; - } - - void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) { - if( !holds( conc ) ) { - Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); - if( d_lemmas_produced.find( lemma ) == d_lemmas_produced.end() ) { - d_lemmas_out.push_back( lemma ); - d_lemmas_produced.insert( lemma ); - Trace("rels-send-lemma") << "[Theory::Rels] **** Generate a lemma conclusion = " << conc << " with reason = " << ant << " by " << c << std::endl; - } - } - } - - void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) { - if( !holds( fact ) ) { - Trace("rels-send-lemma") << "[Theory::Rels] **** Generate an infered fact " - << fact << " with reason " << exp << " by "<< c << std::endl; - d_pending_facts[fact] = exp; - } else { - Trace("rels-send-lemma-debug") << "[Theory::Rels] **** Generate an infered fact " - << fact << " with reason " << exp << " by "<< c - << ", but it holds already, thus skip it!" << std::endl; - } - } - Node TheorySetsRels::getRepresentative( Node t ) { if( d_eqEngine->hasTerm( t ) ){ return d_eqEngine->getRepresentative( t ); @@ -1138,37 +1138,19 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti return false; } - void TheorySetsRels::addToMap(std::map< Node, std::vector >& map, Node rel_rep, Node member) { - if(map.find(rel_rep) == map.end()) { - std::vector members; - members.push_back(member); - map[rel_rep] = members; - } else { - map[rel_rep].push_back(member); - } - } - - void TheorySetsRels::addSharedTerm( TNode n ) { - Trace("rels-debug") << "[sets-rels] Add a shared term: " << n << std::endl; - d_sets_theory.addSharedTerm(n); - d_eqEngine->addTriggerTerm(n, THEORY_SETS); - } - void TheorySetsRels::makeSharedTerm( Node n ) { - Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl; if(d_shared_terms.find(n) == d_shared_terms.end()) { + Trace("rels-share") << " [sets-rels] making shared term " << n + << std::endl; Node skolem = NodeManager::currentNM()->mkSkolem( "sts", NodeManager::currentNM()->mkSetType( n.getType() ) ); - sendLemma(skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON,n)), d_trueNode, "share-term"); + Node skEq = + skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON, n)); + // force lemma to be sent immediately + d_sets_theory.getOutputChannel()->lemma(skEq); d_shared_terms.insert(n); } } - bool TheorySetsRels::holds(Node node) { - bool polarity = node.getKind() != kind::NOT; - Node atom = polarity ? node : node[0]; - return d_sets_theory.isEntailed( atom, polarity ); - } - /* * For each tuple n, we store a mapping between n and a list of its elements representatives * in d_tuple_reps. This would later be used for applying JOIN operator. @@ -1198,42 +1180,11 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); tuple_reduct = NodeManager::currentNM()->mkNode(kind::MEMBER,tuple_reduct, n[1]); Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::EQUAL, n, tuple_reduct); - sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); + sendInfer(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); d_symbolic_tuples.insert(n); } } - TheorySetsRels::TheorySetsRels( context::Context* c, - context::UserContext* u, - eq::EqualityEngine* eq, - context::CDO* conflict, - TheorySets& d_set ): - d_eqEngine(eq), - d_conflict(conflict), - d_sets_theory(d_set), - d_trueNode(NodeManager::currentNM()->mkConst(true)), - d_falseNode(NodeManager::currentNM()->mkConst(false)), - d_pending_merge(c), - d_lemmas_produced(u), - d_shared_terms(u) - { - d_eqEngine->addFunctionKind(kind::PRODUCT); - 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() { - for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); - i != iend; ++i){ - EqcInfo* current = (*i).second; - Assert(current != NULL); - delete current; - } - } - std::vector TupleTrie::findTerms( std::vector< Node >& reps, int argIndex ) { std::vector nodes; std::map< Node, TupleTrie >::iterator it; @@ -1317,368 +1268,12 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti } } - TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) : - d_mem(c), d_mem_exp(c), d_tp(c), d_pt(c), d_tc(c), d_rel_tc(c) {} - - void TheorySetsRels::eqNotifyNewClass( Node n ) { - Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl; - if(n.getKind() == kind::TRANSPOSE || n.getKind() == kind::PRODUCT || n.getKind() == kind::TCLOSURE) { - getOrMakeEqcInfo( n, true ); - if( n.getKind() == kind::TCLOSURE ) { - Node relRep_of_tc = getRepresentative( n[0] ); - EqcInfo* rel_ei = getOrMakeEqcInfo( relRep_of_tc, true ); - - if( rel_ei->d_rel_tc.get().isNull() ) { - rel_ei->d_rel_tc = n; - Node exp = relRep_of_tc == n[0] ? d_trueNode : NodeManager::currentNM()->mkNode( kind::EQUAL, relRep_of_tc, n[0] ); - for( NodeSet::const_iterator mem_it = rel_ei->d_mem.begin(); mem_it != rel_ei->d_mem.end(); mem_it++ ) { - Node mem_exp = (*rel_ei->d_mem_exp.find(*mem_it)).second; - exp = NodeManager::currentNM()->mkNode( kind::AND, exp, mem_exp); - if( mem_exp[1] != relRep_of_tc ) { - exp = NodeManager::currentNM()->mkNode( kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, relRep_of_tc, mem_exp[1] ) ); - } - sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, mem_exp[0], n), exp, "TCLOSURE-UP I" ); - } - } - } - } - } - - // Merge t2 into t1, t1 will be the rep of the new eqc - void TheorySetsRels::eqNotifyPostMerge( Node t1, Node t2 ) { - Trace("rels-std") << "[sets-rels-std] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; - - // Merge membership constraint with "true" eqc - if( t1 == d_trueNode && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple() ) { - Node mem_rep = getRepresentative( t2[0] ); - Node t2_1rep = getRepresentative( t2[1] ); - EqcInfo* ei = getOrMakeEqcInfo( t2_1rep, true ); - if(ei->d_mem.contains(mem_rep)) { - return; - } - Node exp = t2; - - ei->d_mem.insert( mem_rep ); - ei->d_mem_exp.insert( mem_rep, exp ); - - // 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() != t2[1] ) { - exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_tp.get(), t2[1]), t2 ); - } - sendInferTranspose( t2[0], ei->d_tp.get(), exp ); - } - // 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() != t2[1] ) { - exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_pt.get(), t2[1]), t2 ); - } - sendInferProduct( t2[0], ei->d_pt.get(), exp ); - } - - if( !ei->d_rel_tc.get().isNull() ) { - if( ei->d_rel_tc.get()[0] != t2[1] ) { - exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_rel_tc.get()[0], t2[1]), t2 ); - } - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t2[0], ei->d_rel_tc.get()), exp, "TCLOSURE-UP I"); - } - // Process a membership constraint that a tuple is a member of transitive closure of rel - if( !ei->d_tc.get().isNull() ) { - sendInferTClosure( t2, ei ); - } - - // Merge two relation eqcs - } else if( t1.getType().isSet() && t2.getType().isSet() && t1.getType().getSetElementType().isTuple() ) { - EqcInfo* t1_ei = getOrMakeEqcInfo( t1 ); - EqcInfo* t2_ei = getOrMakeEqcInfo( t2 ); - - if( t1_ei != NULL && t2_ei != NULL ) { - if( !t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { - sendInferTranspose(t1_ei->d_tp.get(), t2_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::EQUAL, t1_ei->d_tp.get(), t2_ei->d_tp.get() ) ); - } - std::vector< Node > t2_new_mems; - std::vector< Node > t2_new_exps; - NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin(); - NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin(); - - for( ; t2_mem_it != t2_ei->d_mem.end(); t2_mem_it++ ) { - if( !t1_ei->d_mem.contains( *t2_mem_it ) ) { - Node t2_mem_exp = (*t2_ei->d_mem_exp.find(*t2_mem_it)).second; - - if( t2_ei->d_tp.get().isNull() && !t1_ei->d_tp.get().isNull() ) { - Node reason = t1_ei->d_tp.get() == (t2_mem_exp)[1] - ? (t2_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t2_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_mem_exp)[1], t1_ei->d_tp.get())); - sendInferTranspose( t2_mem_exp[0], t1_ei->d_tp.get(), reason ); - } - if( t2_ei->d_pt.get().isNull() && !t1_ei->d_pt.get().isNull() ) { - Node reason = t1_ei->d_pt.get() == (t2_mem_exp)[1] - ? (t2_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t2_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_mem_exp)[1], t1_ei->d_pt.get())); - sendInferProduct( t2_mem_exp[0], t1_ei->d_pt.get(), reason ); - } - if( t2_ei->d_tc.get().isNull() && !t1_ei->d_tc.get().isNull() ) { - sendInferTClosure( t2_mem_exp, t1_ei ); - } - if( t2_ei->d_rel_tc.get().isNull() && !t1_ei->d_rel_tc.get().isNull() ) { - Node reason = t1_ei->d_rel_tc.get()[0] == t2_mem_exp[1] ? - t2_mem_exp : NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, t1_ei->d_rel_tc.get()[0], t2_mem_exp[1]), t2_mem_exp ); - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t2_mem_exp[0], t1_ei->d_rel_tc.get()), reason, "TCLOSURE-UP I"); - } - t2_new_mems.push_back( *t2_mem_it ); - t2_new_exps.push_back( t2_mem_exp ); - } - } - for( ; t1_mem_it != t1_ei->d_mem.end(); t1_mem_it++ ) { - if( !t2_ei->d_mem.contains( *t1_mem_it ) ) { - Node t1_mem_exp = (*t1_ei->d_mem_exp.find(*t1_mem_it)).second; - if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { - Node reason = t2_ei->d_tp.get() == (t1_mem_exp)[1] - ? (t1_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t1_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_mem_exp)[1], t2_ei->d_tp.get())); - sendInferTranspose( (t1_mem_exp)[0], t2_ei->d_tp.get(), reason ); - } - if( t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) { - Node reason = t2_ei->d_pt.get() == (t1_mem_exp)[1] - ? (t1_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t1_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_mem_exp)[1], t2_ei->d_pt.get())); - sendInferProduct( (t1_mem_exp)[0], t2_ei->d_pt.get(), reason ); - } - if( t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) { - sendInferTClosure(t1_mem_exp, t2_ei ); - } - if( t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) { - Node reason = t2_ei->d_rel_tc.get()[0] == t1_mem_exp[1] ? - t1_mem_exp : NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, t2_ei->d_rel_tc.get()[0], t1_mem_exp[1]), t1_mem_exp ); - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t1_mem_exp[0], t2_ei->d_rel_tc.get()), reason, "TCLOSURE-UP I"); - } - } - } - std::vector< Node >::iterator t2_new_mem_it = t2_new_mems.begin(); - std::vector< Node >::iterator t2_new_exp_it = t2_new_exps.begin(); - for( ; t2_new_mem_it != t2_new_mems.end(); t2_new_mem_it++, t2_new_exp_it++ ) { - t1_ei->d_mem.insert( *t2_new_mem_it ); - t1_ei->d_mem_exp.insert( *t2_new_mem_it, *t2_new_exp_it ); - } - if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { - t1_ei->d_tp.set(t2_ei->d_tp.get()); - } - if( t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) { - t1_ei->d_pt.set(t2_ei->d_pt.get()); - } - if( t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) { - t1_ei->d_tc.set(t2_ei->d_tc.get()); - } - if( t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) { - t1_ei->d_rel_tc.set(t2_ei->d_rel_tc.get()); - } - } else if( t1_ei != NULL ) { - if( (t2.getKind() == kind::TRANSPOSE && t1_ei->d_tp.get().isNull()) || - (t2.getKind() == kind::PRODUCT && t1_ei->d_pt.get().isNull()) || - (t2.getKind() == kind::TCLOSURE && t1_ei->d_tc.get().isNull()) ) { - NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin(); - - if( t2.getKind() == kind::TRANSPOSE ) { - t1_ei->d_tp = t2; - } else if( t2.getKind() == kind::PRODUCT ) { - t1_ei->d_pt = t2; - } else if( t2.getKind() == kind::TCLOSURE ) { - t1_ei->d_tc = t2; - } - for( ; t1_mem_it != t1_ei->d_mem.end(); t1_mem_it++ ) { - Node t1_exp = (*t1_ei->d_mem_exp.find(*t1_mem_it)).second; - if( t2.getKind() == kind::TRANSPOSE ) { - Node reason = t2 == t1_exp[1] - ? (t1_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t1_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_exp)[1], t2)); - sendInferTranspose( (t1_exp)[0], t2, reason ); - } else if( t2.getKind() == kind::PRODUCT ) { - Node reason = t2 == (t1_exp)[1] - ? (t1_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t1_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_exp)[1], t2)); - sendInferProduct( (t1_exp)[0], t2, reason ); - } else if( t2.getKind() == kind::TCLOSURE ) { - sendInferTClosure( t1_exp, t1_ei ); - } - } - } - } else if( t2_ei != NULL ) { - EqcInfo* new_t1_ei = getOrMakeEqcInfo( t1, true ); - if( new_t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { - new_t1_ei->d_tp.set(t2_ei->d_tp.get()); - } - if( new_t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) { - new_t1_ei->d_pt.set(t2_ei->d_pt.get()); - } - if( new_t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) { - new_t1_ei->d_tc.set(t2_ei->d_tc.get()); - } - if( new_t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) { - new_t1_ei->d_rel_tc.set(t2_ei->d_rel_tc.get()); - } - if( (t1.getKind() == kind::TRANSPOSE && t2_ei->d_tp.get().isNull()) || - (t1.getKind() == kind::PRODUCT && t2_ei->d_pt.get().isNull()) || - (t1.getKind() == kind::TCLOSURE && t2_ei->d_tc.get().isNull()) ) { - NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin(); - - for( ; t2_mem_it != t2_ei->d_mem.end(); t2_mem_it++ ) { - Node t2_exp = (*t1_ei->d_mem_exp.find(*t2_mem_it)).second; - - if( t1.getKind() == kind::TRANSPOSE ) { - Node reason = t1 == (t2_exp)[1] - ? (t2_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t2_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_exp)[1], t1)); - sendInferTranspose( (t2_exp)[0], t1, reason ); - } else if( t1.getKind() == kind::PRODUCT ) { - Node reason = t1 == (t2_exp)[1] - ? (t2_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t2_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_exp)[1], t1)); - sendInferProduct( (t2_exp)[0], t1, reason ); - } else if( t1.getKind() == kind::TCLOSURE ) { - sendInferTClosure( t2_exp, new_t1_ei ); - } - } - } - } - } - - Trace("rels-std") << "[sets-rels] done with eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; - } - - void TheorySetsRels::sendInferTClosure( Node new_mem_exp, EqcInfo* ei ) { - NodeSet::const_iterator mem_it = ei->d_mem.begin(); - Node mem_rep = getRepresentative( new_mem_exp[0] ); - Node new_mem_rel = new_mem_exp[1]; - Node new_mem_fst = RelsUtils::nthElementOfTuple( new_mem_exp[0], 0 ); - Node new_mem_snd = RelsUtils::nthElementOfTuple( new_mem_exp[0], 1 ); - for( ; mem_it != ei->d_mem.end(); mem_it++ ) { - if( *mem_it == mem_rep ) { - continue; - } - Node d_mem_exp = (*ei->d_mem_exp.find(*mem_it)).second; - Node d_mem_fst = RelsUtils::nthElementOfTuple( d_mem_exp[0], 0 ); - Node d_mem_snd = RelsUtils::nthElementOfTuple( d_mem_exp[0], 1 ); - Node d_mem_rel = d_mem_exp[1]; - if( areEqual( new_mem_fst, d_mem_snd) ) { - Node reason = NodeManager::currentNM()->mkNode( kind::AND, new_mem_exp, d_mem_exp ); - reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_fst, d_mem_snd ) ); - if( new_mem_rel != ei->d_tc.get() ) { - reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_rel, ei->d_tc.get() ) ); - } - if( d_mem_rel != ei->d_tc.get() ) { - reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, d_mem_rel, ei->d_tc.get() ) ); - } - Node new_membership = NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( d_mem_rel, d_mem_fst, new_mem_snd ), ei->d_tc.get() ); - sendMergeInfer( new_membership, reason, "TCLOSURE-UP II" ); - } - if( areEqual( new_mem_snd, d_mem_fst ) ) { - Node reason = NodeManager::currentNM()->mkNode( kind::AND, new_mem_exp, d_mem_exp ); - reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_snd, d_mem_fst ) ); - if( new_mem_rel != ei->d_tc.get() ) { - reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_rel, ei->d_tc.get() ) ); - } - if( d_mem_rel != ei->d_tc.get() ) { - reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, d_mem_rel, ei->d_tc.get() ) ); - } - Node new_membership = NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( d_mem_rel, new_mem_fst, d_mem_snd ), ei->d_tc.get() ); - sendMergeInfer( new_membership, reason, "TCLOSURE-UP II" ); - } - } - } - - - void TheorySetsRels::doPendingMerge() { - for( NodeList::const_iterator itr = d_pending_merge.begin(); itr != d_pending_merge.end(); itr++ ) { - if( !holds(*itr) ) { - if( d_lemmas_produced.find(*itr)==d_lemmas_produced.end() ) { - Trace("rels-std-lemma") << "[std-sets-rels-lemma] Send out a merge fact as lemma: " - << *itr << std::endl; - d_sets_theory.d_out->lemma( *itr ); - d_lemmas_produced.insert(*itr); - } - } - } - } - - // t1 and t2 can be both relations - // or t1 is a tuple, t2 is a transposed relation - void TheorySetsRels::sendInferTranspose( Node t1, Node t2, Node exp ) { - Assert( t2.getKind() == kind::TRANSPOSE ); - - if( isRel(t1) && isRel(t2) ) { - Assert(t1.getKind() == kind::TRANSPOSE); - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, t1[0], t2[0]), exp, "Transpose-Equal"); - return; - } - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(t1), t2[0]), exp, "Transpose-Rule"); - } - - void TheorySetsRels::sendMergeInfer( Node fact, Node reason, const char * c ) { - if( !holds( fact ) ) { - Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, reason, fact); - d_pending_merge.push_back(lemma); - Trace("rels-std") << "[std-rels-lemma] Generate a lemma by applying " << c - << ": " << lemma << std::endl; - } - } - - void TheorySetsRels::sendInferProduct( Node member, Node pt_rel, Node exp ) { - Assert( pt_rel.getKind() == kind::PRODUCT ); - - std::vector r1_element; - std::vector r2_element; - Node r1 = pt_rel[0]; - Node r2 = pt_rel[1]; - Datatype dt = r1.getType().getSetElementType().getDatatype(); - unsigned int i = 0; - unsigned int s1_len = r1.getType().getSetElementType().getTupleLength(); - unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength(); - - r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); - for( ; i < s1_len; ++i ) { - r1_element.push_back( RelsUtils::nthElementOfTuple( member, i ) ); - } - - dt = r2.getType().getSetElementType().getDatatype(); - r2_element.push_back( Node::fromExpr( dt[0].getConstructor() ) ); - for( ; i < tup_len; ++i ) { - r2_element.push_back( RelsUtils::nthElementOfTuple(member, i) ); - } - - Node tuple_1 = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, r1_element ); - Node tuple_2 = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, r2_element ); - sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_1, r1), exp, "Product-Split" ); - sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_2, r2), exp, "Product-Split" ); - } - - TheorySetsRels::EqcInfo* TheorySetsRels::getOrMakeEqcInfo( Node n, bool doMake ){ - std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); - if( eqc_i == d_eqc_info.end() ){ - if( doMake ){ - EqcInfo* ei; - if( eqc_i!=d_eqc_info.end() ){ - ei = eqc_i->second; - }else{ - ei = new EqcInfo(d_sets_theory.getSatContext()); - d_eqc_info[n] = ei; - } - if( n.getKind() == kind::TRANSPOSE ){ - ei->d_tp = n; - } else if( n.getKind() == kind::PRODUCT ) { - ei->d_pt = n; - } else if( n.getKind() == kind::TCLOSURE ) { - ei->d_tc = n; - } - return ei; - }else{ - return NULL; - } - }else{ - return (*eqc_i).second; - } - } - - void TheorySetsRels::printNodeMap(const char* fst, - const char* snd, - const NodeMap& map) + void TheorySetsRels::sendInfer(Node fact, Node reason, const char* c) { - for (const auto& key_data : map) - { - Trace("rels-debug") << fst << " " << key_data.first << " " << snd << " " - << key_data.second << std::endl; - } + Trace("rels-lemma") << "Rels::lemma " << fact << " from " << reason + << " by " << c << std::endl; + Node lemma = NodeManager::currentNM()->mkNode(IMPLIES, reason, fact); + d_pending.push_back(lemma); } } } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 7cad0f18d..d4a91007b 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -29,8 +29,7 @@ namespace CVC4 { namespace theory { namespace sets { -class TheorySets; - +class TheorySetsPrivate; class TupleTrie { public: @@ -45,63 +44,52 @@ public: void clear() { d_data.clear(); } };/* class TupleTrie */ +/** The relations extension of the theory of sets + * + * This class implements inference schemes described in Meng et al. CADE 2017 + * for handling quantifier-free constraints in the theory of relations. + * + * In CVC4, relations are represented as sets of tuples. The theory of + * relations includes constraints over operators, e.g. TRANSPOSE, JOIN and so + * on, which apply to sets of tuples. + * + * Since relations are a special case of sets, this class is implemented as an + * extension of the theory of sets. That is, it shares many components of the + * TheorySets object which owns it. + */ class TheorySetsRels { typedef context::CDList NodeList; typedef context::CDHashSet< Node, NodeHashFunction > NodeSet; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; public: - TheorySetsRels(context::Context* c, - context::UserContext* u, - eq::EqualityEngine*, - context::CDO*, - TheorySets&); - - ~TheorySetsRels(); - void check(Theory::Effort); - void doPendingLemmas(); - - bool isRelationKind( Kind k ); -private: - /** equivalence class info - * d_mem tuples that are members of this equivalence class - * 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_tc is a node of kind TCLOSURE (if any) in this equivalence class, - */ - class EqcInfo - { - public: - EqcInfo( context::Context* c ); - ~EqcInfo(){} - NodeSet d_mem; - NodeMap d_mem_exp; - context::CDO< Node > d_tp; - context::CDO< Node > d_pt; - context::CDO< Node > d_tc; - context::CDO< Node > d_rel_tc; - }; + TheorySetsRels(context::Context* c, + context::UserContext* u, + eq::EqualityEngine* eq, + TheorySetsPrivate& set); + + ~TheorySetsRels(); + /** + * Invoke the check method with effort level e. At a high level, this class + * will make calls to TheorySetsPrivate::processInference to assert facts, + * lemmas, and conflicts. If this class makes no such call, then the current + * set of assertions is satisfiable with respect to relations. + */ + void check(Theory::Effort e); + /** Is kind k a kind that belongs to the relation theory? */ + static bool isRelationKind(Kind k); private: - - /** has eqc info */ - bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); } - - eq::EqualityEngine *d_eqEngine; - context::CDO *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 */ - NodeList d_pending_merge; - NodeSet d_lemmas_produced; + /** The parent theory of sets object */ + TheorySetsPrivate& d_sets_theory; + /** pointer to the equality engine of the theory of sets */ + eq::EqualityEngine* d_eqEngine; + /** A list of pending inferences to process */ + std::vector d_pending; NodeSet d_shared_terms; - std::vector< Node > d_lemmas_out; - std::map< Node, Node > d_pending_facts; std::unordered_set< Node, NodeHashFunction > d_rel_nodes; @@ -124,24 +112,27 @@ private: std::map< Node, std::map< Node, std::unordered_set > > d_rRep_tcGraph; std::map< Node, std::map< Node, std::unordered_set > > d_tcr_tcGraph; std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps; - std::map< Node, std::vector< Node > > d_tc_lemmas_last; - std::map< Node, EqcInfo* > d_eqc_info; - -public: - /** Standard effort notifications */ - void eqNotifyNewClass(Node t); - void eqNotifyPostMerge(Node t1, Node t2); - -private: - - /** Methods used in standard effort */ - void doPendingMerge(); - void sendInferProduct(Node member, Node pt_rel, Node exp); - void sendInferTranspose(Node t1, Node t2, Node exp ); - void sendInferTClosure( Node mem_rep, EqcInfo* ei ); - void sendMergeInfer( Node fact, Node reason, const char * c ); - EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); + context::Context* d_satContext; + + private: + /** Send infer + * + * Called when we have inferred fact from explanation reason, where the + * latter should be a conjunction of facts that hold in the current context. + * + * The argument c is used for debugging, to give the name of the inference + * rule being used. + * + * This method adds the node (=> reason exp) to the pending vector d_pending. + */ + void sendInfer(Node fact, Node reason, const char* c); + /** + * This method flushes the inferences in the pending vector d_pending to + * theory of sets, which may process them as lemmas or as facts to assert to + * the equality engine. + */ + void doPendingInfers(); /** Methods used in full effort */ void check(); @@ -169,14 +160,7 @@ private: void isTCReachable( Node start, Node dest, std::unordered_set& hasSeen, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); - - void addSharedTerm( TNode n ); - void sendInfer( Node fact, Node exp, const char * c ); - void sendLemma( Node fact, Node reason, const char * c ); - void doTCLemmas(); - /** Helper functions */ - bool holds( Node ); bool hasTerm( Node a ); void makeSharedTerm( Node ); void reduceTupleVar( Node ); @@ -184,13 +168,8 @@ private: void computeTupleReps( Node ); bool areEqual( Node a, Node b ); Node getRepresentative( Node t ); - bool exists( std::vector&, Node ); inline void addToMembershipDB( Node, Node, Node ); - static void printNodeMap(const char* fst, - const char* snd, - const NodeMap& map); inline Node constructPair(Node tc_rep, Node a, Node b); - void addToMap( std::map< Node, std::vector >&, Node, Node ); bool safelyAddToMap( std::map< Node, std::vector >&, Node, Node ); bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();} }; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index a21edd8eb..1bd8bb247 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1566,8 +1566,22 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ if( !d_conflict ){ if( options::ufssMode()==UF_SS_FULL ){ Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl; - if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){ - debugPrint( "uf-ss-debug" ); + if (level == Theory::EFFORT_FULL) + { + if (Debug.isOn("uf-ss-debug")) + { + debugPrint("uf-ss-debug"); + } + if (Trace.isOn("uf-ss-state")) + { + Trace("uf-ss-state") + << "StrongSolverTheoryUF::check " << level << std::endl; + for (std::pair& rm : d_rep_model) + { + Trace("uf-ss-state") << " " << rm.first << " has cardinality " + << rm.second->getCardinality() << std::endl; + } + } } for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ it->second->check( level, d_out );