diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/uf | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/Makefile.am | 10 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 34 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 165 | ||||
-rw-r--r-- | src/theory/uf/inst_strategy.cpp | 412 | ||||
-rw-r--r-- | src/theory/uf/inst_strategy.h | 179 | ||||
-rw-r--r-- | src/theory/uf/kinds | 5 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 88 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 89 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_candidate_generator.cpp | 170 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_candidate_generator.h | 115 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.cpp | 520 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.h | 201 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 1267 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 322 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 14 |
16 files changed, 3576 insertions, 25 deletions
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 50147b997..2c9cd3b80 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -14,6 +14,14 @@ libuf_la_SOURCES = \ equality_engine_types.h \ equality_engine.cpp \ symmetry_breaker.h \ - symmetry_breaker.cpp + symmetry_breaker.cpp \ + theory_uf_instantiator.h \ + theory_uf_instantiator.cpp \ + theory_uf_strong_solver.h \ + theory_uf_strong_solver.cpp \ + theory_uf_candidate_generator.h \ + theory_uf_candidate_generator.cpp \ + inst_strategy.h \ + inst_strategy.cpp EXTRA_DIST = kinds diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 25645c472..96c8e8b59 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -211,6 +211,11 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { Debug("equality") << d_name << "::eq::newNode(" << node << ") => " << newId << std::endl; + // notify e.g. the UF theory strong solver + if (d_performNotify) { + d_notify.eqNotifyNewClass(node); + } + return newId; } @@ -346,7 +351,12 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { if (hasTerm(eq[0]) && hasTerm(eq[1]) && areDisequal(eq[0], eq[1], false)) { return; } - + + // notify the theory + if (d_performNotify) { + d_notify.eqNotifyDisequal(eq[0], eq[1], reason); + } + Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; assertEqualityInternal(eq, d_false, reason); @@ -437,6 +447,21 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect EqualityNodeId class1Id = class1.getFind(); EqualityNodeId class2Id = class2.getFind(); + Node n1 = d_nodes[class1Id]; + Node n2 = d_nodes[class2Id]; + EqualityNode cc1 = getEqualityNode(n1); + EqualityNode cc2 = getEqualityNode(n2); + bool doNotify = false; + // notify the theory + // the second part of this check is needed due to the internal implementation of this class. + // It ensures that we are merging terms and not operators. + if (d_performNotify && class1Id==cc1.getFind() && class2Id==cc2.getFind()) { + doNotify = true; + } + if (doNotify) { + d_notify.eqNotifyPreMerge(n1, n2); + } + // Check for constant merges bool class1isConstant = d_isConstant[class1Id]; bool class2isConstant = d_isConstant[class2Id]; @@ -559,7 +584,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Now merge the lists class1.merge<true>(class2); - + + // notify the theory + if (doNotify) { + d_notify.eqNotifyPostMerge(n1, n2); + } + // Go through the trigger term disequalities and propagate if (!propagateTriggerTermDisequalities(class1OnlyTags, class1triggerRef, class2disequalitiesToNotify)) { return false; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 8cf159cd7..cb0c81872 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -39,6 +39,9 @@ namespace CVC4 { namespace theory { namespace eq { +class EqClassesIterator; +class EqClassIterator; + /** * Interface for equality engine notifications. All the notifications * are safe as TNodes, but not necessarily for negations. @@ -62,7 +65,7 @@ public: /** * Notifies about a trigger predicate that became true or false. * - * @param predicate the trigger predicate that bacame true or false + * @param predicate the trigger predicate that became true or false * @param value the value of the predicate */ virtual bool eqNotifyTriggerPredicate(TNode predicate, bool value) = 0; @@ -82,10 +85,43 @@ public: * can do is ask for explanations. * * @param t1 a constant term - * @param t2 a constnat term + * @param t2 a constant term */ virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0; -}; + + /** + * Notifies about the creation of a new equality class. + * + * @param t the term forming the new class + */ + virtual void eqNotifyNewClass(TNode t) = 0; + + /** + * Notifies about the merge of two classes (just before the merge). + * + * @param t1 a term + * @param t2 a term + */ + virtual void eqNotifyPreMerge(TNode t1, TNode t2) = 0; + + /** + * Notifies about the merge of two classes (just after the merge). + * + * @param t1 a term + * @param t2 a term + */ + virtual void eqNotifyPostMerge(TNode t1, TNode t2) = 0; + + /** + * Notifies about the disequality of two terms. + * + * @param t1 a term + * @param t2 a term + * @param reason the reason + */ + virtual void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) = 0; + +};/* class EqualityEngineNotify */ /** * Implementation of the notification interface that ignores all the @@ -97,7 +133,11 @@ public: bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; } void eqNotifyConstantTermMerge(TNode t1, TNode t2) { } -}; + void eqNotifyNewClass(TNode t) { } + void eqNotifyPreMerge(TNode t1, TNode t2) { } + void eqNotifyPostMerge(TNode t1, TNode t2) { } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } +};/* class EqualityEngineNotifyNone */ /** @@ -106,6 +146,9 @@ public: */ class EqualityEngine : public context::ContextNotifyObj { + friend class EqClassesIterator; + friend class EqClassIterator; + /** Default implementation of the notification object */ static EqualityEngineNotifyNone s_notifyNone; @@ -140,14 +183,14 @@ public: StatisticsRegistry::unregisterStat(&functionTermsCount); StatisticsRegistry::unregisterStat(&constantTermsCount); } - }; + };/* struct EqualityEngine::statistics */ /** * Store the application lookup, with enough information to backtrack */ void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId); -private: +//private: /** The context we are using */ context::Context* d_context; @@ -212,7 +255,7 @@ private: /** Equality constructor */ Equality(EqualityNodeId lhs = null_id, EqualityNodeId rhs = null_id) : lhs(lhs), rhs(rhs) {} - }; + };/* struct EqualityEngine::Equality */ /** The ids of the classes we have merged */ std::vector<Equality> d_assertedEqualities; @@ -253,7 +296,7 @@ private: /** The reason of this edge */ TNode getReason() const { return d_reason; } -}; + };/* class EqualityEngine::EqualityEdge */ /** * All the equality edges (twice as many as the number of asserted equalities. If an equality @@ -268,7 +311,7 @@ private: std::string edgesToString(EqualityEdgeId edgeId) const; /** - * Map from a node to it's first edge in the equality graph. Edges are added to the front of the + * Map from a node to its first edge in the equality graph. Edges are added to the front of the * list which makes the insertion/backtracking easy. */ std::vector<EqualityEdgeId> d_equalityGraph; @@ -297,7 +340,7 @@ private: */ bool merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggers); - /** Undo the mereg of class2 into class1 */ + /** Undo the merge of class2 into class1 */ void undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id); /** Backtrack the information if necessary */ @@ -314,7 +357,7 @@ private: Trigger(EqualityNodeId classId = null_id, TriggerId nextTrigger = null_trigger) : classId(classId), nextTrigger(nextTrigger) {} - }; + };/* struct EqualityEngine::Trigger */ /** * Vector of triggers. Triggers come in pairs for an @@ -436,7 +479,7 @@ private: EqualityNodeId getTrigger(TheoryId tag) const { return triggers[Theory::setIndex(tag, tags)]; } - }; + };/* struct EqualityEngine::TriggerTermSet */ /** Internal tags for creating a new set */ Theory::Set d_newSetTags; @@ -451,7 +494,7 @@ private: char* d_triggerDatabase; /** Allocated size of the trigger term database */ - DefaultSizeType d_triggerDatabaseAllocatedSize ; + DefaultSizeType d_triggerDatabaseAllocatedSize; /** Reference for the trigger terms set */ typedef DefaultSizeType TriggerTermSetRef; @@ -482,7 +525,7 @@ private: TriggerTermSetRef oldValue; TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id) : classId(classId), oldValue(oldValue) {} - }; + };/* struct EqualityEngine::TriggerSetUpdate */ /** * List of trigger updates for backtracking. @@ -685,7 +728,7 @@ public: * Add term to the set of trigger terms with a corresponding tag. The notify class will get * notified when two trigger terms with the same tag become equal or dis-equal. The notification * will not happen on all the terms, but only on the ones that are represent the class. Note that - * a term can be added more than once with different tags, and each tag apperance will merit + * a term can be added more than once with different tags, and each tag appearance will merit * it's own notification. * * @param t the trigger term @@ -743,7 +786,97 @@ public: }; -} // Namespace uf +class EqClassesIterator { + + eq::EqualityEngine* d_ee; + size_t d_it; + +public: + + EqClassesIterator() { } + EqClassesIterator(eq::EqualityEngine* ee) : d_ee(ee) { + d_it = 0; + if ( d_it < d_ee->d_nodesCount && + d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it] ) { + ++*this; + } + } + Node operator*() { + return d_ee->d_nodes[d_it]; + } + bool operator==(const EqClassesIterator& i) { + return d_ee == i.d_ee && d_it == i.d_it; + } + bool operator!=(const EqClassesIterator& i) { + return !(*this == i); + } + EqClassesIterator& operator++() { + Node orig = d_ee->d_nodes[d_it]; + ++d_it; + while ( d_it<d_ee->d_nodesCount && + ( d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it] + || d_ee->d_nodes[d_it] == orig ) ) { // this line is necessary for ignoring duplicates + ++d_it; + } + return *this; + } + EqClassesIterator operator++(int) { + EqClassesIterator i = *this; + ++*this; + return i; + } + bool isFinished() { + return d_it>=d_ee->d_nodesCount; + } +};/* class EqClassesIterator */ + +class EqClassIterator { + + Node d_rep; + eq::EqualityNode d_curr; + Node d_curr_node; + eq::EqualityEngine* d_ee; + +public: + + EqClassIterator() { } + EqClassIterator(Node eqc, eq::EqualityEngine* ee) : d_ee(ee) { + Assert( d_ee->getRepresentative(eqc) == eqc ); + d_rep = eqc; + d_curr_node = eqc; + d_curr = d_ee->getEqualityNode(eqc); + } + Node operator*() { + return d_curr_node; + } + bool operator==(const EqClassIterator& i) { + return d_ee == i.d_ee && d_curr_node == i.d_curr_node; + } + bool operator!=(const EqClassIterator& i) { + return !(*this == i); + } + EqClassIterator& operator++() { + Node next = d_ee->d_nodes[ d_curr.getNext() ]; + Assert( d_rep==d_ee->getRepresentative(next) ); + if (d_rep != next) { // we end when we have cycled back to the original representative + d_curr_node = next; + d_curr = d_ee->getEqualityNode(d_curr.getNext()); + } else { + d_curr_node = Node::null(); + } + return *this; + } + EqClassIterator operator++(int) { + EqClassIterator i = *this; + ++*this; + return i; + } + bool isFinished() { + return d_curr_node == Node::null(); + } +};/* class EqClassIterator */ + +} // Namespace eq } // Namespace theory } // Namespace CVC4 diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp new file mode 100644 index 000000000..2ca2dcb5a --- /dev/null +++ b/src/theory/uf/inst_strategy.cpp @@ -0,0 +1,412 @@ +/********************* */ +/*! \file inst_strategy.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory uf instantiation strategies + **/ + +#include "theory/uf/inst_strategy.h" + +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/equality_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; + +#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER +//#define MULTI_TRIGGER_FULL_EFFORT_HALF +#define MULTI_MULTI_TRIGGERS + +struct sortQuantifiersForSymbol { + QuantifiersEngine* d_qe; + bool operator() (Node i, Node j) { + int nqfsi = d_qe->getNumQuantifiersForSymbol( i.getOperator() ); + int nqfsj = d_qe->getNumQuantifiersForSymbol( j.getOperator() ); + if( nqfsi<nqfsj ){ + return true; + }else if( nqfsi>nqfsj ){ + return false; + }else{ + return false; + } + } +}; + + +void InstStrategyCheckCESolved::processResetInstantiationRound( Theory::Effort effort ){ + for( std::map< Node, bool >::iterator it = d_solved.begin(); it != d_solved.end(); ++it ){ + calcSolved( it->first ); + } +} + +int InstStrategyCheckCESolved::process( Node f, Theory::Effort effort, int e, int instLimit ){ + if( e==0 ){ + //calc solved if not done so already + if( d_solved.find( f )==d_solved.end() ){ + calcSolved( f ); + } + //check if f is counterexample-solved + Debug("quant-uf-strategy") << "Try CE-solved.." << std::endl; + if( d_solved[ f ] ){ + if( d_quantEngine->addInstantiation( f, d_th->d_baseMatch[f] ) ){ + ++(d_th->d_statistics.d_instantiations_ce_solved); + //d_quantEngine->d_hasInstantiated[f] = true; + } + d_solved[f] = false; + } + Debug("quant-uf-strategy") << "done." << std::endl; + } + return STATUS_UNKNOWN; +} + +void InstStrategyCheckCESolved::calcSolved( Node f ){ + d_th->d_baseMatch[f].clear(); + d_solved[ f ]= true; + //check if instantiation constants are solved for + for( int j = 0; j<(int)d_quantEngine->getNumInstantiationConstants( f ); j++ ){ + Node i = d_quantEngine->getInstantiationConstant( f, j ); + Node rep = d_th->getInternalRepresentative( i ); + if( !rep.hasAttribute(InstConstantAttribute()) ){ + d_th->d_baseMatch[f].d_map[ i ] = rep; + }else{ + d_solved[ f ] = false; + } + } +} + +void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){ + //reset triggers + for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){ + for( int i=0; i<(int)it->second.size(); i++ ){ + it->second[i]->resetInstantiationRound(); + it->second[i]->reset( Node::null() ); + } + } +} + +int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e, int instLimit ){ + if( e==0 ){ + return STATUS_UNFINISHED; + }else if( e==1 ){ + d_counter[f]++; + Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl; + //Notice() << "Try user-provided patterns..." << std::endl; + for( int i=0; i<(int)d_user_gen[f].size(); i++ ){ + bool processTrigger = true; + if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){ +//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF +// processTrigger = d_counter[f]%2==0; +//#endif + } + if( processTrigger ){ + //if( d_user_gen[f][i]->isMultiTrigger() ) + //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl; + int numInst = d_user_gen[f][i]->addInstantiations( d_th->d_baseMatch[f], instLimit ); + //if( d_user_gen[f][i]->isMultiTrigger() ) + //Notice() << " Done, numInst = " << numInst << "." << std::endl; + d_th->d_statistics.d_instantiations_user_pattern += numInst; + if( d_user_gen[f][i]->isMultiTrigger() ){ + d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; + } + //d_quantEngine->d_hasInstantiated[f] = true; + } + } + Debug("quant-uf-strategy") << "done." << std::endl; + //Notice() << "done" << std::endl; + } + return STATUS_UNKNOWN; +} + +void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ + //add to generators + std::vector< Node > nodes; + for( int i=0; i<(int)pat.getNumChildren(); i++ ){ + nodes.push_back( pat[i] ); + } + if( Trigger::isUsableTrigger( nodes, f ) ){ + //extend to literal matching + d_quantEngine->getPhaseReqTerms( f, nodes ); + //check match option + int matchOption = Options::current()->efficientEMatching ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; + d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, + Options::current()->smartTriggers ) ); + } +} + +void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){ + //reset triggers + for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){ + for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){ + itt->first->resetInstantiationRound(); + itt->first->reset( Node::null() ); + } + } +} + +int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e, int instLimit ){ + int peffort = f.getNumChildren()==3 ? 2 : 1; + //int peffort = f.getNumChildren()==3 ? 2 : 1; + //int peffort = 1; + if( e<peffort ){ + return STATUS_UNFINISHED; + }else{ + bool gen = false; + if( e==peffort ){ + if( d_counter.find( f )==d_counter.end() ){ + d_counter[f] = 0; + gen = true; + }else{ + d_counter[f]++; + gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0; + } + }else{ + gen = true; + } + if( gen ){ + generateTriggers( f ); + } + Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl; + //Notice() << "Try auto-generated triggers..." << std::endl; + for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){ + Trigger* tr = itt->first; + if( tr ){ + bool processTrigger = itt->second; + if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){ +#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF + processTrigger = d_counter[f]%2==0; +#endif + } + if( processTrigger ){ + //if( tr->isMultiTrigger() ) + Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl; + int numInst = tr->addInstantiations( d_th->d_baseMatch[f], instLimit ); + //if( tr->isMultiTrigger() ) + Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl; + if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ + d_th->d_statistics.d_instantiations_auto_gen_min += numInst; + }else{ + d_th->d_statistics.d_instantiations_auto_gen += numInst; + } + if( tr->isMultiTrigger() ){ + d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; + } + //d_quantEngine->d_hasInstantiated[f] = true; + } + } + } + Debug("quant-uf-strategy") << "done." << std::endl; + //Notice() << "done" << std::endl; + } + return STATUS_UNKNOWN; +} + +void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ + Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl; + if( d_patTerms[0].find( f )==d_patTerms[0].end() ){ + //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy + d_patTerms[0][f].clear(); + d_patTerms[1][f].clear(); + std::vector< Node > patTermsF; + Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getCounterexampleBody( f ), patTermsF, d_tr_strategy, true ); + Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getCounterexampleBody( f ) << std::endl; + Debug("auto-gen-trigger") << " "; + for( int i=0; i<(int)patTermsF.size(); i++ ){ + Debug("auto-gen-trigger") << patTermsF[i] << " "; + } + Debug("auto-gen-trigger") << std::endl; + //extend to literal matching + d_quantEngine->getPhaseReqTerms( f, patTermsF ); + //sort into single/multi triggers + std::map< Node, std::vector< Node > > varContains; + Trigger::getVarContains( f, patTermsF, varContains ); + for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ + if( it->second.size()==f[0].getNumChildren() ){ + d_patTerms[0][f].push_back( it->first ); + d_is_single_trigger[ it->first ] = true; + }else{ + d_patTerms[1][f].push_back( it->first ); + d_is_single_trigger[ it->first ] = false; + } + } + d_made_multi_trigger[f] = false; + Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl; + Debug("auto-gen-trigger") << " "; + for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ + Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " "; + } + Debug("auto-gen-trigger") << std::endl; + Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl; + Debug("auto-gen-trigger") << " "; + for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){ + Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " "; + } + Debug("auto-gen-trigger") << std::endl; + } + + //populate candidate pattern term vector for the current trigger + std::vector< Node > patTerms; +#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER + //try to add single triggers first + for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ + if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){ + patTerms.push_back( d_patTerms[0][f][i] ); + } + } + //if no single triggers exist, add multi trigger terms + if( patTerms.empty() ){ + patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() ); + } +#else + patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() ); + patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() ); +#endif + + if( !patTerms.empty() ){ + Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl; + //sort terms based on relevance + if( d_rlv_strategy==RELEVANCE_DEFAULT ){ + sortQuantifiersForSymbol sqfs; + sqfs.d_qe = d_quantEngine; + //sort based on # occurrences (this will cause Trigger to select rarer symbols) + std::sort( patTerms.begin(), patTerms.end(), sqfs ); + Debug("relevant-trigger") << "Terms based on relevance: " << std::endl; + for( int i=0; i<(int)patTerms.size(); i++ ){ + Debug("relevant-trigger") << " " << patTerms[i] << " ("; + Debug("relevant-trigger") << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl; + } + //Notice() << "Terms based on relevance: " << std::endl; + //for( int i=0; i<(int)patTerms.size(); i++ ){ + // Notice() << " " << patTerms[i] << " ("; + // Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl; + //} + } + //now, generate the trigger... + int matchOption = Options::current()->efficientEMatching ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; + Trigger* tr = NULL; + if( d_is_single_trigger[ patTerms[0] ] ){ + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, + Options::current()->smartTriggers ); + d_single_trigger_gen[ patTerms[0] ] = true; + }else{ + //if we are re-generating triggers, shuffle based on some method + if( d_made_multi_trigger[f] ){ +#ifndef MULTI_MULTI_TRIGGERS + return; +#endif + std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly + }else{ + d_made_multi_trigger[f] = true; + } + //will possibly want to get an old trigger + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, + Options::current()->smartTriggers ); + } + if( tr ){ + if( tr->isMultiTrigger() ){ + //disable all other multi triggers + for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){ + if( it->first->isMultiTrigger() ){ + d_auto_gen_trigger[f][ it->first ] = false; + } + } + } + //making it during an instantiation round, so must reset + if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){ + tr->resetInstantiationRound(); + tr->reset( Node::null() ); + } + d_auto_gen_trigger[f][tr] = true; + //if we are generating additional triggers... + if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){ + int index = 0; + if( index<(int)patTerms.size() ){ + //Notice() << "check add additional" << std::endl; + //check if similar patterns exist, and if so, add them additionally + int nqfs_curr = d_quantEngine->getNumQuantifiersForSymbol( patTerms[0].getOperator() ); + index++; + bool success = true; + while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){ + success = false; + if( d_quantEngine->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ + d_single_trigger_gen[ patTerms[index] ] = true; + Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, + Options::current()->smartTriggers ); + if( tr2 ){ + //Notice() << "Add additional trigger " << patTerms[index] << std::endl; + tr2->resetInstantiationRound(); + tr2->reset( Node::null() ); + d_auto_gen_trigger[f][tr2] = true; + } + success = true; + } + index++; + } + //Notice() << "done check add additional" << std::endl; + } + } + } + } +} + +#if 0 + +void InstStrategyAddFailSplits::processResetInstantiationRound( Theory::Effort effort ){ +} + +int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e, int instLimit ){ + if( e<4 ){ + return STATUS_UNFINISHED; + }else{ + for( std::map< Node, std::map< Node, std::vector< InstMatchGenerator* > > >::iterator it = InstMatchGenerator::d_match_fails.begin(); + it != InstMatchGenerator::d_match_fails.end(); ++it ){ + for( std::map< Node, std::vector< InstMatchGenerator* > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + if( !it2->second.empty() ){ + Node n1 = it->first; + Node n2 = it2->first; + if( !d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ) && !d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ) ){ + d_quantEngine->addSplitEquality( n1, n2, true ); + } + it2->second.clear(); + } + } + } + return STATUS_UNKNOWN; + } +} + +#endif /* 0 */ + +void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ +} + +int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e, int instLimit ){ + if( e<5 ){ + return STATUS_UNFINISHED; + }else{ + if( d_guessed.find( f )==d_guessed.end() ){ + d_guessed[f] = true; + Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl; + InstMatch m; + if( d_quantEngine->addInstantiation( f, m ) ){ + ++(d_th->d_statistics.d_instantiations_guess); + //d_quantEngine->d_hasInstantiated[f] = true; + } + } + return STATUS_UNKNOWN; + } +} diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h new file mode 100644 index 000000000..906169811 --- /dev/null +++ b/src/theory/uf/inst_strategy.h @@ -0,0 +1,179 @@ +/********************* */ +/*! \file inst_strategy.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory uf instantiation strategies + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__INST_STRATEGY_H +#define __CVC4__INST_STRATEGY_H + +#include "theory/quantifiers_engine.h" + +#include "context/context.h" +#include "context/context_mm.h" + +#include "util/stats.h" +#include "theory/uf/theory_uf.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class InstantiatorTheoryUf; + +//instantiation strategies + +class InstStrategyCheckCESolved : public InstStrategy{ +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** is solved? */ + std::map< Node, bool > d_solved; + /** calc if f is solved */ + void calcSolved( Node f ); + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ){} + ~InstStrategyCheckCESolved(){} + /** identify */ + std::string identify() const { return std::string("CheckCESolved"); } +};/* class InstStrategyCheckCESolved */ + +class InstStrategyUserPatterns : public InstStrategy{ +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** explicitly provided patterns */ + std::map< Node, std::vector< Trigger* > > d_user_gen; + /** counter for quantifiers */ + std::map< Node, int > d_counter; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + InstStrategyUserPatterns( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ){} + ~InstStrategyUserPatterns(){} +public: + /** add pattern */ + void addUserPattern( Node f, Node pat ); + /** get num patterns */ + int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); } + /** get user pattern */ + Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; } + /** identify */ + std::string identify() const { return std::string("UserPatterns"); } +};/* class InstStrategyUserPatterns */ + +class InstStrategyAutoGenTriggers : public InstStrategy{ +public: + enum { + RELEVANCE_NONE, + RELEVANCE_DEFAULT, + }; +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** trigger generation strategy */ + int d_tr_strategy; + /** relevance strategy */ + int d_rlv_strategy; + /** regeneration */ + bool d_regenerate; + int d_regenerate_frequency; + /** generate additional triggers */ + bool d_generate_additional; + /** triggers for each quantifier */ + std::map< Node, std::map< Trigger*, bool > > d_auto_gen_trigger; + std::map< Node, int > d_counter; + /** single, multi triggers for each quantifier */ + std::map< Node, std::vector< Node > > d_patTerms[2]; + std::map< Node, bool > d_is_single_trigger; + std::map< Node, bool > d_single_trigger_gen; + std::map< Node, bool > d_made_multi_trigger; +private: + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); + /** generate triggers */ + void generateTriggers( Node f ); +public: + InstStrategyAutoGenTriggers( InstantiatorTheoryUf* th, QuantifiersEngine* ie, int tstrt, int rstrt, int rgfr = -1 ) : + InstStrategy( ie ), d_th( th ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){ + setRegenerateFrequency( rgfr ); + } + ~InstStrategyAutoGenTriggers(){} +public: + /** get auto-generated trigger */ + Trigger* getAutoGenTrigger( Node f ); + /** identify */ + std::string identify() const { return std::string("AutoGenTriggers"); } + /** set regenerate frequency, if fr<0, turn off regenerate */ + void setRegenerateFrequency( int fr ){ + if( fr<0 ){ + d_regenerate = false; + }else{ + d_regenerate_frequency = fr; + d_regenerate = true; + } + } + /** set generate additional */ + void setGenerateAdditional( bool val ) { d_generate_additional = val; } +};/* class InstStrategyAutoGenTriggers */ + +#if 0 + +class InstStrategyAddFailSplits : public InstStrategy{ +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ){} + ~InstStrategyAddFailSplits(){} + /** identify */ + std::string identify() const { return std::string("AddFailSplits"); } +};/* class InstStrategyAddFailSplits */ + +#endif /* 0 */ + +class InstStrategyFreeVariable : public InstStrategy{ +private: + /** InstantiatorTheoryUf class */ + InstantiatorTheoryUf* d_th; + /** guessed instantiations */ + std::map< Node, bool > d_guessed; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + InstStrategyFreeVariable( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ){} + ~InstStrategyFreeVariable(){} + /** identify */ + std::string identify() const { return std::string("FreeVariable"); } +};/* class InstStrategyFreeVariable */ + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 2de3715e1..ec353dc59 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -6,6 +6,7 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" typechecker "theory/uf/theory_uf_type_rules.h" +instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h" properties stable-infinite parametric properties check propagate staticLearning presolve @@ -15,4 +16,8 @@ parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule +operator CARDINALITY_CONSTRAINT 2 "cardinality constraint" + +typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule + endtheory diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 5761ee4f5..26678f21d 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -443,6 +443,16 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { Assert(p.size() > 1); + // check that the types match + Permutation::iterator permIt = p.begin(); + TypeNode type = (*permIt++).getType(); + do { + if(type != (*permIt++).getType()) { + Debug("ufsymm") << "UFSYMM types don't match, aborting.." << endl; + return false; + } + } while(permIt != p.end()); + // check P_swap vector<Node> subs; vector<Node> repls; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 7583f8ee7..dc7bb7c92 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -18,6 +18,8 @@ **/ #include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/uf/theory_uf_strong_solver.h" using namespace std; using namespace CVC4; @@ -25,8 +27,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ -TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_UF, c, u, out, valuation, logicInfo), +TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : + Theory(THEORY_UF, c, u, out, valuation, logicInfo, qe), d_notify(*this), d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"), d_conflict(c, false), @@ -36,6 +38,12 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); + + if (Options::current()->finiteModelFind) { + d_thss = new StrongSolverTheoryUf(c, u, out, this); + } else { + d_thss = NULL; + } }/* TheoryUF::TheoryUF() */ static Node mkAnd(const std::vector<TNode>& conjunctions) { @@ -62,29 +70,46 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) { void TheoryUF::check(Effort level) { - while (!done() && !d_conflict) + while (!done() && !d_conflict) { // Get all the assertions Assertion assertion = get(); TNode fact = assertion.assertion; Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl; + if (d_thss != NULL) { + bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); + d_thss->assertNode(fact, isDecision); + } // Do the work bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); + } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT) { + // do nothing } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } } + + if (d_thss != NULL) { + if (! d_conflict) { + d_thss->check(level); + } + } + }/* TheoryUF::check() */ void TheoryUF::preRegisterTerm(TNode node) { Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl; + if (d_thss != NULL) { + d_thss->preRegisterTerm(node); + } + switch (node.getKind()) { case kind::EQUAL: // Add the trigger for equality @@ -124,6 +149,12 @@ bool TheoryUF::propagate(TNode literal) { return ok; }/* TheoryUF::propagate(TNode) */ +void TheoryUF::propagate(Effort effort) { + if (d_thss != NULL) { + return d_thss->propagate(effort); + } +} + void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) { // Do the work bool polarity = literal.getKind() != kind::NOT; @@ -395,3 +426,54 @@ void TheoryUF::conflict(TNode a, TNode b) { d_out->conflict(d_conflictNode); d_conflict = true; } + +void TheoryUF::eqNotifyNewClass(TNode t) { + if (d_thss != NULL) { + d_thss->newEqClass(t); + } + // this can be called very early, during initialization + if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) { + ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t); + } +} + +void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) { + if (getLogicInfo().isQuantified()) { + ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2); + } +} + +void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) { + if (d_thss != NULL) { + d_thss->merge(t1, t2); + } +} + +void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + if (d_thss != NULL) { + d_thss->assertDisequal(t1, t2, reason); + } + if (getLogicInfo().isQuantified()) { + ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason); + } +} + +Node TheoryUF::ppRewrite(TNode node) { + + if (node.getKind() != kind::APPLY_UF) { + return node; + } + + // perform the callbacks requested by TheoryUF::registerPpRewrite() + RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator()); + if (c == d_registeredPpRewrites.end()) { + return node; + } else { + Node res = c->second->ppRewrite(node); + if (res != node) { + return ppRewrite(res); + } else { + return res; + } + } +} diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index eceead38a..a55ef92b5 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -36,7 +36,15 @@ namespace CVC4 { namespace theory { namespace uf { +class UfTermDb; +class InstantiatorTheoryUf; +class StrongSolverTheoryUf; + class TheoryUF : public Theory { + + friend class InstantiatorTheoryUf; + friend class StrongSolverTheoryUf; + public: class NotifyClass : public eq::EqualityEngineNotify { @@ -76,13 +84,43 @@ public: Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.conflict(t1, t2); } - }; + + void eqNotifyNewClass(TNode t) { + Debug("uf") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; + d_uf.eqNotifyNewClass(t); + } + + void eqNotifyPreMerge(TNode t1, TNode t2) { + Debug("uf") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; + d_uf.eqNotifyPreMerge(t1, t2); + } + + void eqNotifyPostMerge(TNode t1, TNode t2) { + Debug("uf") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; + d_uf.eqNotifyPostMerge(t1, t2); + } + + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + Debug("uf") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; + d_uf.eqNotifyDisequal(t1, t2, reason); + } + + };/* class TheoryUF::NotifyClass */ + + /** A callback class for ppRewrite(). See registerPpRewrite(), below. */ + class PpRewrite { + public: + virtual Node ppRewrite(TNode node) = 0; + };/* class TheoryUF::PpRewrite */ private: /** The notify class */ NotifyClass d_notify; + /** The associated theory strong solver (or NULL if none) */ + StrongSolverTheoryUf* d_thss; + /** Equaltity engine */ eq::EqualityEngine d_equalityEngine; @@ -118,10 +156,37 @@ private: /** Conflict when merging two constants */ void conflict(TNode a, TNode b); + /** called when a new equivalance class is created */ + void eqNotifyNewClass(TNode t); + + /** called when two equivalance classes will merge */ + void eqNotifyPreMerge(TNode t1, TNode t2); + + /** called when two equivalance classes have merged */ + void eqNotifyPostMerge(TNode t1, TNode t2); + + /** called when two equivalence classes are made disequal */ + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + + /** a registry type for keeping Node-specific callbacks for ppRewrite() */ + typedef std::hash_map<Node, PpRewrite*, NodeHashFunction> RegisterPpRewrites; + + /** a collection of callbacks to issue while doing a ppRewrite() */ + RegisterPpRewrites d_registeredPpRewrites; + public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + + ~TheoryUF() { + // destruct all ppRewrite() callbacks + for(RegisterPpRewrites::iterator i = d_registeredPpRewrites.begin(); + i != d_registeredPpRewrites.end(); + ++i) { + delete i->second; + } + } void check(Effort); void preRegisterTerm(TNode term); @@ -133,7 +198,7 @@ public: void addSharedTerm(TNode n); void computeCareGraph(); - void propagate(Effort effort) {} + void propagate(Effort effort); EqualityStatus getEqualityStatus(TNode a, TNode b); @@ -141,6 +206,24 @@ public: return "THEORY_UF"; } + eq::EqualityEngine* getEqualityEngine() { + return &d_equalityEngine; + } + + StrongSolverTheoryUf* getStrongSolver() { + return d_thss; + } + + Node ppRewrite(TNode node); + + /** + * Register a ppRewrite() callback on "op." TheoryUF owns + * the callback, and will delete it when it is destructed. + */ + void registerPpRewrite(TNode op, PpRewrite* callback) { + d_registeredPpRewrites.insert(std::make_pair(op, callback)); + } + };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ diff --git a/src/theory/uf/theory_uf_candidate_generator.cpp b/src/theory/uf/theory_uf_candidate_generator.cpp new file mode 100644 index 000000000..e8aa98aa7 --- /dev/null +++ b/src/theory/uf/theory_uf_candidate_generator.cpp @@ -0,0 +1,170 @@ +/********************* */ +/*! \file theory_uf_candidate_generator.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory uf candidate generator class + **/ + +#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; + +CandidateGeneratorTheoryUf::CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op ) : + d_op( op ), d_ith( ith ), d_term_iter( -2 ){ + Assert( !d_op.isNull() ); +} +void CandidateGeneratorTheoryUf::resetInstantiationRound(){ + d_term_iter_limit = d_ith->getQuantifiersEngine()->getTermDatabase()->d_op_map[d_op].size(); +} + +void CandidateGeneratorTheoryUf::reset( Node eqc ){ + if( eqc.isNull() ){ + d_term_iter = 0; + }else{ + //create an equivalence class iterator in eq class eqc + if( ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->hasTerm( eqc ) ){ + eqc = ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->getRepresentative( eqc ); + d_eqc = eq::EqClassIterator( eqc, ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() ); + d_retNode = Node::null(); + }else{ + d_retNode = eqc; + } + d_term_iter = -1; + } +} + +Node CandidateGeneratorTheoryUf::getNextCandidate(){ + if( d_term_iter>=0 ){ + //get next candidate term in the uf term database + while( d_term_iter<d_term_iter_limit ){ + Node n = d_ith->getQuantifiersEngine()->getTermDatabase()->d_op_map[d_op][d_term_iter]; + d_term_iter++; + if( isLegalCandidate( n ) ){ + return n; + } + } + }else if( d_term_iter==-1 ){ + if( d_retNode.isNull() ){ + //get next candidate term in equivalence class + while( !d_eqc.isFinished() ){ + Node n = (*d_eqc); + ++d_eqc; + if( n.getKind()==APPLY_UF && n.getOperator()==d_op ){ + if( isLegalCandidate( n ) ){ + return n; + } + } + } + }else{ + Node ret; + if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){ + ret = d_retNode; + } + d_term_iter = -2; //done returning matches + return ret; + } + } + return Node::null(); +} + + +//CandidateGeneratorTheoryUfDisequal::CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc ) : +// d_ith( ith ), d_eq_class( eqc ){ +// d_eci = NULL; +//} +//void CandidateGeneratorTheoryUfDisequal::resetInstantiationRound(){ +// +//} +////we will iterate over all terms that are disequal from eqc +//void CandidateGeneratorTheoryUfDisequal::reset( Node eqc ){ +// //Assert( !eqc.isNull() ); +// ////begin iterating over equivalence classes that are disequal from eqc +// //d_eci = d_ith->getEquivalenceClassInfo( eqc ); +// //if( d_eci ){ +// // d_eqci_iter = d_eci->d_disequal.begin(); +// //} +//} +//Node CandidateGeneratorTheoryUfDisequal::getNextCandidate(){ +// //if( d_eci ){ +// // while( d_eqci_iter != d_eci->d_disequal.end() ){ +// // if( (*d_eqci_iter).second ){ +// // //we have an equivalence class that is disequal from eqc +// // d_cg->reset( (*d_eqci_iter).first ); +// // Node n = d_cg->getNextCandidate(); +// // //if there is a candidate in this equivalence class, return it +// // if( !n.isNull() ){ +// // return n; +// // } +// // } +// // ++d_eqci_iter; +// // } +// //} +// return Node::null(); +//} + + +CandidateGeneratorTheoryUfLitEq::CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat ) : + d_match_pattern( mpat ), d_ith( ith ){ + +} +void CandidateGeneratorTheoryUfLitEq::resetInstantiationRound(){ + +} +void CandidateGeneratorTheoryUfLitEq::reset( Node eqc ){ + d_eq = eq::EqClassesIterator( ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() ); +} +Node CandidateGeneratorTheoryUfLitEq::getNextCandidate(){ + while( d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType()==d_match_pattern[0].getType() ){ + //an equivalence class with the same type as the pattern, return reflexive equality + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); + } + } + return Node::null(); +} + + +CandidateGeneratorTheoryUfLitDeq::CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat ) : + d_match_pattern( mpat ), d_ith( ith ){ + +} +void CandidateGeneratorTheoryUfLitDeq::resetInstantiationRound(){ + +} +void CandidateGeneratorTheoryUfLitDeq::reset( Node eqc ){ + Node false_term = ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->getRepresentative( + NodeManager::currentNM()->mkConst<bool>(false) ); + d_eqc_false = eq::EqClassIterator( false_term, ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() ); +} +Node CandidateGeneratorTheoryUfLitDeq::getNextCandidate(){ + //get next candidate term in equivalence class + while( !d_eqc_false.isFinished() ){ + Node n = (*d_eqc_false); + ++d_eqc_false; + if( n.getKind()==d_match_pattern.getKind() ){ + //found an iff or equality, try to match it + //DO_THIS: cache to avoid redundancies? + //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? + return n; + } + } + return Node::null(); +} diff --git a/src/theory/uf/theory_uf_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h new file mode 100644 index 000000000..948573439 --- /dev/null +++ b/src/theory/uf/theory_uf_candidate_generator.h @@ -0,0 +1,115 @@ +/********************* */ +/*! \file theory_uf_candidate generator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory uf candidate generator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H +#define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H + +#include "theory/quantifiers_engine.h" +#include "theory/uf/theory_uf_instantiator.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class CandidateGeneratorTheoryUfDisequal; + +class CandidateGeneratorTheoryUf : public CandidateGenerator +{ + friend class CandidateGeneratorTheoryUfDisequal; +private: + //operator you are looking for + Node d_op; + //instantiator pointer + InstantiatorTheoryUf* d_ith; + //the equality class iterator + eq::EqClassIterator d_eqc; + int d_term_iter; + int d_term_iter_limit; +private: + Node d_retNode; +public: + CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op ); + ~CandidateGeneratorTheoryUf(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +//class CandidateGeneratorTheoryUfDisequal : public CandidateGenerator +//{ +//private: +// //equivalence class +// Node d_eq_class; +// //equivalence class info +// EqClassInfo* d_eci; +// //equivalence class iterator +// EqClassInfo::BoolMap::const_iterator d_eqci_iter; +// //instantiator pointer +// InstantiatorTheoryUf* d_ith; +//public: +// CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc ); +// ~CandidateGeneratorTheoryUfDisequal(){} +// +// void resetInstantiationRound(); +// void reset( Node eqc ); //should be what you want to be disequal from +// Node getNextCandidate(); +//}; + +class CandidateGeneratorTheoryUfLitEq : public CandidateGenerator +{ +private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + //einstantiator pointer + InstantiatorTheoryUf* d_ith; +public: + CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat ); + ~CandidateGeneratorTheoryUfLitEq(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +class CandidateGeneratorTheoryUfLitDeq : public CandidateGenerator +{ +private: + //the equality class iterator for false + eq::EqClassIterator d_eqc_false; + //equality you are trying to match disequalities for + Node d_match_pattern; + //einstantiator pointer + InstantiatorTheoryUf* d_ith; +public: + CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat ); + ~CandidateGeneratorTheoryUfLitDeq(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + + +} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp new file mode 100644 index 000000000..9fdcb5952 --- /dev/null +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -0,0 +1,520 @@ +/********************* */ +/*! \file theory_uf_instantiator.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory uf instantiator class + **/ + +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/equality_engine.h" +//#include "theory/uf/inst_strategy_model_find.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; + +EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_disequal( c ){ + +} + +//set member +void EqClassInfo::setMember( Node n, TermDb* db ){ + if( n.getKind()==APPLY_UF ){ + d_funs[n.getOperator()] = true; + } + //add parent functions + for( std::map< Node, std::map< int, std::vector< Node > > >::iterator it = db->d_parents[n].begin(); + it != db->d_parents[n].end(); ++it ){ + d_pfuns[ it->first ] = true; + } +} + +//get has function +bool EqClassInfo::hasFunction( Node op ){ + return d_funs.find( op )!=d_funs.end(); +} + +bool EqClassInfo::hasParent( Node op ){ + return d_pfuns.find( op )!=d_pfuns.end(); +} + +//merge with another eq class info +void EqClassInfo::merge( EqClassInfo* eci ){ + for( BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) { + d_funs[ (*it).first ] = true; + } + for( BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) { + d_pfuns[ (*it).first ] = true; + } +} + +InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) : +Instantiator( c, qe, th ) +{ + qe->setEqualityQuery( new EqualityQueryInstantiatorTheoryUf( this ) ); + + if( Options::current()->finiteModelFind ){ + //if( Options::current()->cbqi ){ + // addInstStrategy( new InstStrategyCheckCESolved( this, qe ) ); + //} + //addInstStrategy( new InstStrategyFiniteModelFind( c, this, ((TheoryUF*)th)->getStrongSolver(), qe ) ); + qe->getTermDatabase()->setMatchingActive( false ); + }else{ + if( Options::current()->cbqi ){ + addInstStrategy( new InstStrategyCheckCESolved( this, qe ) ); + } + if( Options::current()->userPatternsQuant ){ + d_isup = new InstStrategyUserPatterns( this, qe ); + addInstStrategy( d_isup ); + }else{ + d_isup = NULL; + } + InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( this, qe, Trigger::TS_ALL, + InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 ); + i_ag->setGenerateAdditional( true ); + addInstStrategy( i_ag ); + //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) ); + addInstStrategy( new InstStrategyFreeVariable( this, qe ) ); + //d_isup->setPriorityOver( i_ag ); + //d_isup->setPriorityOver( i_agm ); + //i_ag->setPriorityOver( i_agm ); + } +} + +void InstantiatorTheoryUf::preRegisterTerm( Node t ){ + //d_quantEngine->addTermToDatabase( t ); +} + +void InstantiatorTheoryUf::assertNode( Node assertion ) +{ + Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl; + //preRegisterTerm( assertion ); + d_quantEngine->addTermToDatabase( assertion ); + if( Options::current()->cbqi ){ + if( assertion.hasAttribute(InstConstantAttribute()) ){ + setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); + }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ + setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) ); + } + } +} + +void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){ + if( d_isup ){ + d_isup->addUserPattern( f, pat ); + } + setHasConstraintsFrom( f ); +} + + +void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){ + d_ground_reps.clear(); +} + +int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e, int instLimit ){ + Debug("quant-uf") << "UF: Try to solve (" << e << ") for " << f << "... " << std::endl; + return InstStrategy::STATUS_SAT; +} + +void InstantiatorTheoryUf::debugPrint( const char* c ) +{ + +} + +bool InstantiatorTheoryUf::hasTerm( Node a ){ + return ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( a ); +} + +bool InstantiatorTheoryUf::areEqual( Node a, Node b ){ + if( hasTerm( a ) && hasTerm( b ) ){ + return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b ); + }else{ + return a==b; + } +} + +bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){ + if( hasTerm( a ) && hasTerm( b ) ){ + return ((TheoryUF*)d_th)->d_equalityEngine.areDisequal( a, b, false ); + }else{ + return false; + } +} + +Node InstantiatorTheoryUf::getRepresentative( Node a ){ + if( hasTerm( a ) ){ + return ((TheoryUF*)d_th)->d_equalityEngine.getRepresentative( a ); + }else{ + return a; + } +} + +Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){ + if( d_ground_reps.find( a )==d_ground_reps.end() ){ + if( !hasTerm( a ) ){ + return a; + }else{ + Node rep = getRepresentative( a ); + if( !rep.hasAttribute(InstConstantAttribute()) ){ + //return the representative of a + d_ground_reps[a] = rep; + return rep; + }else{ + //otherwise, must search eq class + eq::EqClassIterator eqc_iter( rep, &((TheoryUF*)d_th)->d_equalityEngine ); + rep = Node::null(); + while( !eqc_iter.isFinished() ){ + if( !(*eqc_iter).hasAttribute(InstConstantAttribute()) ){ + d_ground_reps[ a ] = *eqc_iter; + return *eqc_iter; + } + eqc_iter++; + } + d_ground_reps[ a ] = a; + } + } + } + return d_ground_reps[a]; +} + +InstantiatorTheoryUf::Statistics::Statistics(): + //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0), + d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0), + d_instantiations_e_induced("InstantiatorTheoryUf::Instantiations_E-Induced", 0), + d_instantiations_user_pattern("InstantiatorTheoryUf::Instantiations_User_Pattern", 0), + d_instantiations_guess("InstantiatorTheoryUf::Instantiations_Free_Var", 0), + d_instantiations_auto_gen("InstantiatorTheoryUf::Instantiations_Auto_Gen", 0), + d_instantiations_auto_gen_min("InstantiatorTheoryUf::Instantiations_Auto_Gen_Min", 0), + d_splits("InstantiatorTheoryUf::Total_Splits", 0) +{ + //StatisticsRegistry::registerStat(&d_instantiations); + StatisticsRegistry::registerStat(&d_instantiations_ce_solved); + StatisticsRegistry::registerStat(&d_instantiations_e_induced); + StatisticsRegistry::registerStat(&d_instantiations_user_pattern ); + StatisticsRegistry::registerStat(&d_instantiations_guess ); + StatisticsRegistry::registerStat(&d_instantiations_auto_gen ); + StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min ); + StatisticsRegistry::registerStat(&d_splits); +} + +InstantiatorTheoryUf::Statistics::~Statistics(){ + //StatisticsRegistry::unregisterStat(&d_instantiations); + StatisticsRegistry::unregisterStat(&d_instantiations_ce_solved); + StatisticsRegistry::unregisterStat(&d_instantiations_e_induced); + StatisticsRegistry::unregisterStat(&d_instantiations_user_pattern ); + StatisticsRegistry::unregisterStat(&d_instantiations_guess ); + StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen ); + StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min ); + StatisticsRegistry::unregisterStat(&d_splits); +} + +/** new node */ +void InstantiatorTheoryUf::newEqClass( TNode n ){ + d_quantEngine->addTermToDatabase( n ); +} + +/** merge */ +void InstantiatorTheoryUf::merge( TNode a, TNode b ){ + if( Options::current()->efficientEMatching ){ + if( a.getKind()!=IFF && a.getKind()!=EQUAL && b.getKind()!=IFF && b.getKind()!=EQUAL ){ + Debug("efficient-e-match") << "Merging " << a << " with " << b << std::endl; + + //determine new candidates for instantiation + computeCandidatesPcPairs( a, b ); + computeCandidatesPcPairs( b, a ); + computeCandidatesPpPairs( a, b ); + computeCandidatesPpPairs( b, a ); + } + //merge eqc_ops of b into a + EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a ); + EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b ); + eci_a->merge( eci_b ); + } +} + +/** assert terms are disequal */ +void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){ + +} + +EqClassInfo* InstantiatorTheoryUf::getEquivalenceClassInfo( Node n ) { + return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n]; +} +EqClassInfo* InstantiatorTheoryUf::getOrCreateEquivalenceClassInfo( Node n ){ + Assert( n==getRepresentative( n ) ); + if( d_eqc_ops.find( n )==d_eqc_ops.end() ){ + EqClassInfo* eci = new EqClassInfo( d_th->getSatContext() ); + eci->setMember( n, d_quantEngine->getTermDatabase() ); + d_eqc_ops[n] = eci; + } + return d_eqc_ops[n]; +} + +void InstantiatorTheoryUf::computeCandidatesPcPairs( Node a, Node b ){ + Debug("efficient-e-match") << "Compute candidates for pc pairs..." << std::endl; + Debug("efficient-e-match") << " Eq class = ["; + outputEqClass( "efficient-e-match", a); + Debug("efficient-e-match") << "]" << std::endl; + EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a ); + EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( a ); + for( BoolMap::iterator it = eci_a->d_funs.begin(); it != eci_a->d_funs.end(); it++ ) { + //the child function: a member of eq_class( a ) has top symbol g, in other words g is in funs( a ) + Node g = (*it).first; + Debug("efficient-e-match") << " Checking application " << g << std::endl; + //look at all parent/child pairs + for( std::map< Node, std::map< Node, std::vector< InvertedPathString > > >::iterator itf = d_pc_pairs[g].begin(); + itf != d_pc_pairs[g].end(); ++itf ){ + //f/g is a parent/child pair + Node f = itf->first; + if( eci_b->hasParent( f ) || true ){ + //DO_THIS: determine if f in pfuns( b ), only do the follow if so + Debug("efficient-e-match") << " Checking parent application " << f << std::endl; + //scan through the list of inverted path strings/candidate generators + for( std::map< Node, std::vector< InvertedPathString > >::iterator cit = itf->second.begin(); + cit != itf->second.end(); ++cit ){ + Node pat = cit->first; + Debug("efficient-e-match") << " Checking pattern " << pat << std::endl; + for( int c=0; c<(int)cit->second.size(); c++ ){ + Debug("efficient-e-match") << " Check inverted path string for pattern "; + outputInvertedPathString( "efficient-e-match", cit->second[c] ); + Debug("efficient-e-match") << std::endl; + + //collect all new relevant terms + std::vector< Node > terms; + terms.push_back( b ); + collectTermsIps( cit->second[c], terms ); + if( !terms.empty() ){ + Debug("efficient-e-match") << " -> Added terms (" << (int)terms.size() << "): "; + //add them as candidates to the candidate generator + for( int t=0; t<(int)terms.size(); t++ ){ + Debug("efficient-e-match") << terms[t] << " "; + //Notice() << "Add candidate (PC) " << terms[t] << std::endl; + for( int cg=0; cg<(int)d_pat_cand_gens[pat].size(); cg++ ){ + d_pat_cand_gens[pat][cg]->addCandidate( terms[t] ); + } + } + Debug("efficient-e-match") << std::endl; + } + } + } + } + } + } +} + +void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a, Node b ){ + Debug("efficient-e-match") << "Compute candidates for pp pairs..." << std::endl; + EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a ); + EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( a ); + for( std::map< Node, std::map< Node, std::map< Node, std::vector< IpsPair > > > >::iterator it = d_pp_pairs.begin(); + it != d_pp_pairs.end(); ++it ){ + Node f = it->first; + if( eci_a->hasParent( f ) ){ + Debug("efficient-e-match") << " Checking parent application " << f << std::endl; + for( std::map< Node, std::map< Node, std::vector< IpsPair > > >::iterator it2 = it->second.begin(); + it2 != it->second.end(); ++it2 ){ + Node g = it2->first; + if( eci_b->hasParent( g ) ){ + Debug("efficient-e-match") << " Checking parent application " << g << std::endl; + //if f in pfuns( a ) and g is in pfuns( b ), only do the follow if so + for( std::map< Node, std::vector< IpsPair > >::iterator cit = it2->second.begin(); + cit != it2->second.end(); ++cit ){ + Node pat = cit->first; + for( int c=0; c<(int)cit->second.size(); c++ ){ + std::vector< Node > a_terms; + a_terms.push_back( a ); + if( !a_terms.empty() ){ + collectTermsIps( cit->second[c].first, a_terms ); + std::vector< Node > b_terms; + b_terms.push_back( b ); + collectTermsIps( cit->second[c].first, b_terms ); + //take intersection + for( int t=0; t<(int)a_terms.size(); t++ ){ + if( std::find( b_terms.begin(), b_terms.end(), a_terms[t] )!=b_terms.end() ){ + //Notice() << "Add candidate (PP) " << a_terms[t] << std::endl; + Debug("efficient-e-match") << " -> Add term " << a_terms[t] << std::endl; + //add to all candidate generators having this term + for( int cg=0; cg<(int)d_pat_cand_gens[pat].size(); cg++ ){ + d_pat_cand_gens[pat][cg]->addCandidate( a_terms[t] ); + } + } + } + } + } + } + } + } + } + } +} + +void InstantiatorTheoryUf::collectTermsIps( InvertedPathString& ips, std::vector< Node >& terms, int index ){ + if( index<(int)ips.size() && !terms.empty() ){ + Debug("efficient-e-match-debug") << "> Process " << index << std::endl; + Node f = ips[index].first; + int arg = ips[index].second; + + //for each term in terms, determine if any term (modulo equality) has parent "f" from position "arg" + bool addRep = ( index!=(int)ips.size()-1 ); + std::vector< Node > newTerms; + for( int t=0; t<(int)terms.size(); t++ ){ + collectParentsTermsIps( terms[t], f, arg, newTerms, addRep ); + } + terms.clear(); + terms.insert( terms.begin(), newTerms.begin(), newTerms.end() ); + + Debug("efficient-e-match-debug") << "> Terms are now: "; + for( int t=0; t<(int)terms.size(); t++ ){ + Debug("efficient-e-match-debug") << terms[t] << " "; + } + Debug("efficient-e-match-debug") << std::endl; + + collectTermsIps( ips, terms, index+1 ); + } +} + +bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, std::vector< Node >& terms, bool addRep, bool modEq ){ + bool addedTerm = false; + if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) && modEq ){ + Assert( getRepresentative( n )==n ); + //collect modulo equality + //DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it + eq::EqClassIterator eqc_iter( getRepresentative( n ), &((TheoryUF*)d_th)->d_equalityEngine ); + while( !eqc_iter.isFinished() ){ + if( collectParentsTermsIps( (*eqc_iter), f, arg, terms, addRep, false ) ){ + //if only one argument, we know we can stop (since all others added will be congruent) + if( f.getType().getNumChildren()==2 ){ + return true; + } + addedTerm = true; + } + eqc_iter++; + } + }else{ + TermDb* db = d_quantEngine->getTermDatabase(); + //see if parent f exists from argument arg + if( db->d_parents.find( n )!=db->d_parents.end() ){ + if( db->d_parents[n].find( f )!=db->d_parents[n].end() ){ + if( db->d_parents[n][f].find( arg )!=db->d_parents[n][f].end() ){ + for( int i=0; i<(int)db->d_parents[n][f][arg].size(); i++ ){ + Node t = db->d_parents[n][f][arg][i]; + if( addRep ){ + t = getRepresentative( t ); + } + if( std::find( terms.begin(), terms.end(), t )==terms.end() ){ + terms.push_back( t ); + } + addedTerm = true; + } + } + } + } + } + return addedTerm; +} + +void InstantiatorTheoryUf::registerPatternElementPairs2( Node opat, Node pat, InvertedPathString& ips, + std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >& ips_map ){ + Assert( pat.getKind()==APPLY_UF ); + //add information for possible pp-pair + for( int i=0; i<(int)pat.getNumChildren(); i++ ){ + if( pat[i].getKind()==INST_CONSTANT ){ + ips_map[ pat[i] ].push_back( std::pair< Node, InvertedPathString >( pat.getOperator(), InvertedPathString( ips ) ) ); + } + } + ips.push_back( std::pair< Node, int >( pat.getOperator(), 0 ) ); + for( int i=0; i<(int)pat.getNumChildren(); i++ ){ + if( pat[i].getKind()==APPLY_UF ){ + ips.back().second = i; + registerPatternElementPairs2( opat, pat[i], ips, ips_map ); + Debug("pattern-element-opt") << "Found pc-pair ( " << pat.getOperator() << ", " << pat[i].getOperator() << " )" << std::endl; + Debug("pattern-element-opt") << " Path = "; + outputInvertedPathString( "pattern-element-opt", ips ); + Debug("pattern-element-opt") << std::endl; + //pat.getOperator() and pat[i].getOperator() are a pc-pair + d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ][opat].push_back( InvertedPathString( ips ) ); + } + } + ips.pop_back(); +} + +void InstantiatorTheoryUf::registerPatternElementPairs( Node pat ){ + InvertedPathString ips; + std::map< Node, std::vector< std::pair< Node, InvertedPathString > > > ips_map; + registerPatternElementPairs2( pat, pat, ips, ips_map ); + for( std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >::iterator it = ips_map.begin(); it != ips_map.end(); ++it ){ + for( int j=0; j<(int)it->second.size(); j++ ){ + for( int k=j+1; k<(int)it->second.size(); k++ ){ + //found a pp-pair + Debug("pattern-element-opt") << "Found pp-pair ( " << it->second[j].first << ", " << it->second[k].first << " )" << std::endl; + Debug("pattern-element-opt") << " Paths = "; + outputInvertedPathString( "pattern-element-opt", it->second[j].second ); + Debug("pattern-element-opt") << " and "; + outputInvertedPathString( "pattern-element-opt", it->second[k].second ); + Debug("pattern-element-opt") << std::endl; + d_pp_pairs[ it->second[j].first ][ it->second[k].first ][pat].push_back( IpsPair( it->second[j].second, it->second[k].second ) ); + } + } + } +} + +void InstantiatorTheoryUf::registerCandidateGenerator( CandidateGenerator* cg, Node pat ){ + Debug("efficient-e-match") << "Register candidate generator..." << pat << std::endl; + if( d_pat_cand_gens.find( pat )==d_pat_cand_gens.end() ){ + registerPatternElementPairs( pat ); + } + d_pat_cand_gens[pat].push_back( cg ); + + //take all terms from the uf term db and add to candidate generator + Node op = pat.getOperator(); + TermDb* db = d_quantEngine->getTermDatabase(); + for( int i=0; i<(int)db->d_op_map[op].size(); i++ ){ + cg->addCandidate( db->d_op_map[op][i] ); + } + d_cand_gens[op].push_back( cg ); + + Debug("efficient-e-match") << "Done." << std::endl; +} + +void InstantiatorTheoryUf::registerTrigger( Trigger* tr, Node op ){ + if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ + d_op_triggers[op].push_back( tr ); + } +} + +void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){ + if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){ + eq::EqClassIterator eqc_iter( getRepresentative( n ), + &((TheoryUF*)d_th)->d_equalityEngine ); + bool firstTime = true; + while( !eqc_iter.isFinished() ){ + if( !firstTime ){ Debug(c) << ", "; } + Debug(c) << (*eqc_iter); + firstTime = false; + eqc_iter++; + } + }else{ + Debug(c) << n; + } +} + +void InstantiatorTheoryUf::outputInvertedPathString( const char* c, InvertedPathString& ips ){ + for( int i=0; i<(int)ips.size(); i++ ){ + if( i>0 ){ Debug( c ) << "."; } + Debug( c ) << ips[i].first << "." << ips[i].second; + } +} diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h new file mode 100644 index 000000000..e50e3823c --- /dev/null +++ b/src/theory/uf/theory_uf_instantiator.h @@ -0,0 +1,201 @@ +/********************* */ +/*! \file theory_uf_instantiator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory uf instantiator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_UF_INSTANTIATOR_H +#define __CVC4__THEORY_UF_INSTANTIATOR_H + +#include "theory/uf/inst_strategy.h" + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.h" + +#include "util/stats.h" +#include "theory/uf/theory_uf.h" + +namespace CVC4 { +namespace theory { + +class TermDb; + +namespace uf { + +class InstantiatorTheoryUf; + +//equivalence class info +class EqClassInfo +{ +public: + typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; + typedef context::CDChunkList<Node> NodeList; +public: + //a list of operators that occur as top symbols in this equivalence class + // Efficient E-Matching for SMT Solvers: "funs" + BoolMap d_funs; + //a list of operators f for which a term of the form f( ... t ... ) exists + // Efficient E-Matching for SMT Solvers: "pfuns" + BoolMap d_pfuns; + //a list of equivalence classes that are disequal + BoolMap d_disequal; +public: + EqClassInfo( context::Context* c ); + ~EqClassInfo(){} + //set member + void setMember( Node n, TermDb* db ); + //has function "funs" + bool hasFunction( Node op ); + //has parent "pfuns" + bool hasParent( Node op ); + //merge with another eq class info + void merge( EqClassInfo* eci ); +}; + +class InstantiatorTheoryUf : public Instantiator{ + friend class ::CVC4::theory::InstMatchGenerator; + friend class ::CVC4::theory::TermDb; +protected: + typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; + typedef context::CDHashMap<Node, int, NodeHashFunction> IntMap; + typedef context::CDChunkList<Node> NodeList; + typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists; + /** map to representatives used */ + std::map< Node, Node > d_ground_reps; +protected: + /** instantiation strategies */ + InstStrategyUserPatterns* d_isup; +public: + InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th); + ~InstantiatorTheoryUf() {} + /** assertNode method */ + void assertNode( Node assertion ); + /** Pre-register a term. Done one time for a Node, ever. */ + void preRegisterTerm( Node t ); + /** identify */ + std::string identify() const { return std::string("InstantiatorTheoryUf"); } + /** debug print */ + void debugPrint( const char* c ); + /** add user pattern */ + void addUserPattern( Node f, Node pat ); +private: + /** reset instantiation */ + void processResetInstantiationRound( Theory::Effort effort ); + /** calculate matches for quantifier f at effort */ + int process( Node f, Theory::Effort effort, int e, int instLimit ); +public: + /** statistics class */ + class Statistics { + public: + //IntStat d_instantiations; + IntStat d_instantiations_ce_solved; + IntStat d_instantiations_e_induced; + IntStat d_instantiations_user_pattern; + IntStat d_instantiations_guess; + IntStat d_instantiations_auto_gen; + IntStat d_instantiations_auto_gen_min; + IntStat d_splits; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +public: + /** the base match */ + std::map< Node, InstMatch > d_baseMatch; +private: + //for each equivalence class + std::map< Node, EqClassInfo* > d_eqc_ops; +public: + /** general queries about equality */ + bool hasTerm( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); + Node getRepresentative( Node a ); + Node getInternalRepresentative( Node a ); + /** new node */ + void newEqClass( TNode n ); + /** merge */ + void merge( TNode a, TNode b ); + /** assert terms are disequal */ + void assertDisequal( TNode a, TNode b, TNode reason ); + /** get equivalence class info */ + EqClassInfo* getEquivalenceClassInfo( Node n ); + EqClassInfo* getOrCreateEquivalenceClassInfo( Node n ); +private: + typedef std::vector< std::pair< Node, int > > InvertedPathString; + typedef std::pair< InvertedPathString, InvertedPathString > IpsPair; + /** Parent/Child Pairs (for efficient E-matching) + So, for example, if we have the pattern f( g( x ) ), then d_pc_pairs[g][f][f( g( x ) )] = { f.0 }. + */ + std::map< Node, std::map< Node, std::map< Node, std::vector< InvertedPathString > > > > d_pc_pairs; + /** Parent/Parent Pairs (for efficient E-matching) */ + std::map< Node, std::map< Node, std::map< Node, std::vector< IpsPair > > > > d_pp_pairs; + /** list of all candidate generators for each operator */ + std::map< Node, std::vector< CandidateGenerator* > > d_cand_gens; + /** map from patterns to candidate generators */ + std::map< Node, std::vector< CandidateGenerator* > > d_pat_cand_gens; + /** helper functions */ + void registerPatternElementPairs2( Node opat, Node pat, InvertedPathString& ips, + std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >& ips_map ); + void registerPatternElementPairs( Node pat ); + /** compute candidates for pc pairs */ + void computeCandidatesPcPairs( Node a, Node b ); + /** compute candidates for pp pairs */ + void computeCandidatesPpPairs( Node a, Node b ); + /** collect terms based on inverted path string */ + void collectTermsIps( InvertedPathString& ips, std::vector< Node >& terms, int index = 0 ); + bool collectParentsTermsIps( Node n, Node f, int arg, std::vector< Node >& terms, bool addRep, bool modEq = true ); +public: + /** Register candidate generator cg for pattern pat. (for use with efficient e-matching) + This request will ensure that calls will be made to cg->addCandidate( n ) for all + ground terms n that are relevant for matching with pat. + */ + void registerCandidateGenerator( CandidateGenerator* cg, Node pat ); +private: + /** triggers */ + std::map< Node, std::vector< Trigger* > > d_op_triggers; +public: + /** register trigger (for eager quantifier instantiation) */ + void registerTrigger( Trigger* tr, Node op ); +public: + /** output eq class */ + void outputEqClass( const char* c, Node n ); + /** output inverted path string */ + void outputInvertedPathString( const char* c, InvertedPathString& ips ); +};/* class InstantiatorTheoryUf */ + +/** equality query object using instantiator theory uf */ +class EqualityQueryInstantiatorTheoryUf : public EqualityQuery +{ +private: + /** pointer to instantiator uf class */ + InstantiatorTheoryUf* d_ith; +public: + EqualityQueryInstantiatorTheoryUf( InstantiatorTheoryUf* ith ) : d_ith( ith ){} + ~EqualityQueryInstantiatorTheoryUf(){} + /** general queries about equality */ + bool hasTerm( Node a ) { return d_ith->hasTerm( a ); } + Node getRepresentative( Node a ) { return d_ith->getRepresentative( a ); } + bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); } + bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); } + Node getInternalRepresentative( Node a ) { return d_ith->getInternalRepresentative( a ); } +}; /* EqualityQueryInstantiatorTheoryUf */ + +} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp new file mode 100644 index 000000000..a793b6a57 --- /dev/null +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -0,0 +1,1267 @@ +/********************* */ +/*! \file theory_uf_strong_solver.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory uf strong solver class + **/ + +#include "theory/uf/theory_uf_strong_solver.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/theory_engine.h" + +//#define USE_REGION_SAT + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; + +void StrongSolverTheoryUf::ConflictFind::Region::takeNode( StrongSolverTheoryUf::ConflictFind::Region* r, Node n ){ + //Debug("uf-ss") << "takeNode " << r << " " << n << std::endl; + //Debug("uf-ss") << "r : " << std::endl; + //r->debugPrint("uf-ss"); + //Debug("uf-ss") << "this : " << std::endl; + //debugPrint("uf-ss"); + Assert( !hasRep( n ) ); + Assert( r->hasRep( n ) ); + //add representative + setRep( n, true ); + //take disequalities from r + RegionNodeInfo* rni = r->d_nodes[n]; + for( int t=0; t<2; t++ ){ + RegionNodeInfo::DiseqList* del = rni->d_disequalities[t]; + for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){ + if( (*it).second ){ + r->setDisequal( n, (*it).first, t, false ); + if( t==0 ){ + if( hasRep( (*it).first ) ){ + setDisequal( (*it).first, n, 0, false ); + setDisequal( (*it).first, n, 1, true ); + setDisequal( n, (*it).first, 1, true ); + }else{ + setDisequal( n, (*it).first, 0, true ); + } + }else{ + r->setDisequal( (*it).first, n, 1, false ); + r->setDisequal( (*it).first, n, 0, true ); + setDisequal( n, (*it).first, 0, true ); + } + } + } + } + //remove representative + r->setRep( n, false ); + //Debug("uf-ss") << "done takeNode " << r << " " << n << std::endl; +} + +void StrongSolverTheoryUf::ConflictFind::Region::combine( StrongSolverTheoryUf::ConflictFind::Region* r ){ + //take all nodes from r + for( std::map< Node, RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){ + if( it->second->d_valid ){ + setRep( it->first, true ); + } + } + for( std::map< Node, RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){ + if( it->second->d_valid ){ + //take disequalities from r + Node n = it->first; + RegionNodeInfo* rni = it->second; + for( int t=0; t<2; t++ ){ + RegionNodeInfo::DiseqList* del = rni->d_disequalities[t]; + for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){ + if( (*it2).second ){ + if( t==0 && hasRep( (*it2).first ) ){ + setDisequal( (*it2).first, n, 0, false ); + setDisequal( (*it2).first, n, 1, true ); + setDisequal( n, (*it2).first, 1, true ); + }else{ + setDisequal( n, (*it2).first, t, true ); + } + } + } + } + } + } + r->d_valid = false; +} + +void StrongSolverTheoryUf::ConflictFind::Region::setRep( Node n, bool valid ){ + Assert( hasRep( n )!=valid ); + if( d_nodes.find( n )==d_nodes.end() && valid ){ + d_nodes[n] = new RegionNodeInfo( d_cf->d_th->getSatContext() ); + } + d_nodes[n]->d_valid = valid; + d_reps_size = d_reps_size + ( valid ? 1 : -1 ); + if( d_testClique.find( n )!=d_testClique.end() && d_testClique[n] ){ + Assert( !valid ); + d_testClique[n] = false; + d_testCliqueSize = d_testCliqueSize - 1; + //remove all splits involving n + for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){ + if( (*it).second ){ + if( (*it).first[0]==n || (*it).first[1]==n ){ + d_splits[ (*it).first ] = false; + d_splitsSize = d_splitsSize - 1; + } + } + } + } +} + +/** setEqual */ +void StrongSolverTheoryUf::ConflictFind::Region::setEqual( Node a, Node b ){ + Assert( hasRep( a ) && hasRep( b ) ); + //move disequalities of b over to a + for( int t=0; t<2; t++ ){ + RegionNodeInfo::DiseqList* del = d_nodes[b]->d_disequalities[t]; + for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){ + if( (*it).second ){ + Node n = (*it).first; + Region* nr = d_cf->d_regions[ d_cf->d_regions_map[ n ] ]; + if( !isDisequal( a, n, t ) ){ + setDisequal( a, n, t, true ); + nr->setDisequal( n, a, t, true ); + } + setDisequal( b, n, t, false ); + nr->setDisequal( n, b, t, false ); + } + } + } + //remove b from representatives + setRep( b, false ); +} + +void StrongSolverTheoryUf::ConflictFind::Region::setDisequal( Node n1, Node n2, int type, bool valid ){ + //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " " << type << " " << valid << std::endl; + //debugPrint("uf-ss-region-debug"); + //Assert( isDisequal( n1, n2, type )!=valid ); + if( isDisequal( n1, n2, type )!=valid ){ //DO_THIS: make assertion + d_nodes[ n1 ]->d_disequalities[type]->setDisequal( n2, valid ); + if( type==0 ){ + d_total_diseq_external = d_total_diseq_external + ( valid ? 1 : -1 ); + }else{ + d_total_diseq_internal = d_total_diseq_internal + ( valid ? 1 : -1 ); + if( valid ){ + //if they are both a part of testClique, then remove split + if( d_testClique.find( n1 )!=d_testClique.end() && d_testClique[n1] && + d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){ + Node eq = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 ); + if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){ + Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2 << std::endl; + d_splits[ eq ] = false; + d_splitsSize = d_splitsSize - 1; + } + } + } + } + } +} + +bool StrongSolverTheoryUf::ConflictFind::Region::isDisequal( Node n1, Node n2, int type ){ + RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->d_disequalities[type]; + return del->d_disequalities.find( n2 )!=del->d_disequalities.end() && del->d_disequalities[n2]; +} + +bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality ){ + if( d_total_diseq_external>=long(cardinality) ){ + //The number of external disequalities is greater than or equal to cardinality. + //Thus, a clique of size cardinality+1 may exist between nodes in d_regions[i] and other regions + //Check if this is actually the case: must have n nodes with outgoing degree (cardinality+1-n) for some n>0 + std::vector< int > degrees; + for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + RegionNodeInfo* rni = it->second; + if( rni->d_valid ){ + if( rni->getNumDisequalities()>=cardinality ){ + int outDeg = rni->getNumExternalDisequalities(); + if( outDeg>=cardinality ){ + //we have 1 node of degree greater than (cardinality) + return true; + }else if( outDeg>0 ){ + degrees.push_back( outDeg ); + if( (int)degrees.size()>=cardinality ){ + //we have (cardinality) nodes of degree 1 + return true; + } + } + } + } + } + std::sort( degrees.begin(), degrees.end() ); + for( int i=0; i<(int)degrees.size(); i++ ){ + if( degrees[i]>=cardinality+1-((int)degrees.size()-i) ){ + return true; + } + } + } + return false; +} + +struct sortInternalDegree { + StrongSolverTheoryUf::ConflictFind::Region* r; + bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumInternalDisequalities()>r->d_nodes[j]->getNumInternalDisequalities());} +}; + + +bool StrongSolverTheoryUf::ConflictFind::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){ + if( d_reps_size>long(cardinality) ){ + if( d_reps_size>long(cardinality) && d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){ + //quick clique check, all reps form a clique + for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + if( it->second->d_valid ){ + clique.push_back( it->first ); + } + } + return true; + }else{ + //build test clique, up to size cardinality+1 + if( d_testCliqueSize<=long(cardinality) ){ + std::vector< Node > newClique; + if( d_testCliqueSize<long(cardinality) ){ + for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + //if not in the test clique, add it to the set of new members + if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){ + newClique.push_back( it->first ); + } + } + //choose remaining nodes with the highest degrees + sortInternalDegree sidObj; + sidObj.r = this; + std::sort( newClique.begin(), newClique.end(), sidObj ); + newClique.erase( newClique.begin() + ( cardinality - d_testCliqueSize ) + 1, newClique.end() ); + }else{ + //scan for the highest degree + int maxDeg = -1; + Node maxNode; + for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + //if not in the test clique, add it to the set of new members + if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){ + if( it->second->getNumInternalDisequalities()>maxDeg ){ + maxDeg = it->second->getNumInternalDisequalities(); + maxNode = it->first; + } + } + } + Assert( maxNode!=Node::null() ); + newClique.push_back( maxNode ); + } + //check splits internal to new members + for( int j=0; j<(int)newClique.size(); j++ ){ + Debug("uf-ss-debug") << "Choose to add clique member " << newClique[j] << std::endl; + for( int k=(j+1); k<(int)newClique.size(); k++ ){ + if( !isDisequal( newClique[j], newClique[k], 1 ) ){ + d_splits[ NodeManager::currentNM()->mkNode( EQUAL, newClique[j], newClique[k] ) ] = true; + d_splitsSize = d_splitsSize + 1; + } + } + //check disequalities with old members + for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){ + if( (*it).second ){ + if( !isDisequal( (*it).first, newClique[j], 1 ) ){ + d_splits[ NodeManager::currentNM()->mkNode( EQUAL, (*it).first, newClique[j] ) ] = true; + d_splitsSize = d_splitsSize + 1; + } + } + } + } + //add new clique members to test clique + for( int j=0; j<(int)newClique.size(); j++ ){ + d_testClique[ newClique[j] ] = true; + d_testCliqueSize = d_testCliqueSize + 1; + } + } + Assert( d_testCliqueSize==long(cardinality+1) ); + if( d_splitsSize==0 ){ + //test clique is a clique + for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){ + if( (*it).second ){ + clique.push_back( (*it).first ); + } + } + return true; + } + } + } + return false; +} + +Node StrongSolverTheoryUf::ConflictFind::Region::getBestSplit(){ + //take the first split you find + for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){ + if( (*it).second ){ + return (*it).first; + } + } + return Node::null(); +} + +void StrongSolverTheoryUf::ConflictFind::Region::addSplit( OutputChannel* out ){ + Node s = getBestSplit(); + //add lemma to output channel + Assert( s!=Node::null() && s.getKind()==EQUAL ); + s = Rewriter::rewrite( s ); + Debug("uf-ss-lemma") << "*** Split on " << s << std::endl; + //Debug("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " "; + //Debug("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl; + //Debug("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; + debugPrint("uf-ss-temp"); + //Notice() << "*** Split on " << s << std::endl; + //split on the equality s + out->split( s ); + //tell the sat solver to explore the equals branch first + out->requirePhase( s, true ); +} + +void StrongSolverTheoryUf::ConflictFind::Region::getRepresentatives( std::vector< Node >& reps ){ + for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + RegionNodeInfo* rni = it->second; + if( rni->d_valid ){ + reps.push_back( it->first ); + } + } +} + +bool StrongSolverTheoryUf::ConflictFind::Region::minimize( OutputChannel* out ){ + if( hasSplits() ){ + addSplit( out ); + return false; + }else{ + return true; + } +} + +void StrongSolverTheoryUf::ConflictFind::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){ + for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + RegionNodeInfo* rni = it->second; + if( rni->d_valid ){ + RegionNodeInfo::DiseqList* del = rni->d_disequalities[0]; + for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){ + if( (*it2).second ){ + num_ext_disequalities[ (*it2).first ]++; + } + } + } + } +} + +void StrongSolverTheoryUf::ConflictFind::Region::debugPrint( const char* c, bool incClique ){ + Debug( c ) << "Num reps: " << d_reps_size << std::endl; + for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + RegionNodeInfo* rni = it->second; + if( rni->d_valid ){ + Node n = it->first; + Debug( c ) << " " << n << std::endl; + for( int i=0; i<2; i++ ){ + Debug( c ) << " " << ( i==0 ? "Ext" : "Int" ) << " disequal:"; + RegionNodeInfo::DiseqList* del = rni->d_disequalities[i]; + for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){ + if( (*it2).second ){ + Debug( c ) << " " << (*it2).first; + } + } + Debug( c ) << ", total = " << del->d_size << std::endl; + } + } + } + Debug( c ) << "Total disequal: " << d_total_diseq_external << " external," << std::endl; + Debug( c ) << " " << d_total_diseq_internal<< " internal." << std::endl; + + if( incClique ){ + Debug( c ) << "Candidate clique members: " << std::endl; + Debug( c ) << " "; + for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++ it ){ + if( (*it).second ){ + Debug( c ) << (*it).first << " "; + } + } + Debug( c ) << ", size = " << d_testCliqueSize << std::endl; + Debug( c ) << "Required splits: " << std::endl; + Debug( c ) << " "; + for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++ it ){ + if( (*it).second ){ + Debug( c ) << (*it).first << " "; + } + } + Debug( c ) << ", size = " << d_splitsSize << std::endl; + } +} + +void StrongSolverTheoryUf::ConflictFind::combineRegions( int ai, int bi ){ + Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl; + Assert( isValid( ai ) && isValid( bi ) ); + for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[bi]->d_nodes.begin(); it != d_regions[bi]->d_nodes.end(); ++it ){ + Region::RegionNodeInfo* rni = it->second; + if( rni->d_valid ){ + d_regions_map[ it->first ] = ai; + } + } + //update regions disequal DO_THIS? + d_regions[ai]->combine( d_regions[bi] ); + d_regions[bi]->d_valid = false; +} + +void StrongSolverTheoryUf::ConflictFind::moveNode( Node n, int ri ){ + Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl; + Assert( isValid( d_regions_map[ n ] ) ); + Assert( isValid( ri ) ); + ////update regions disequal DO_THIS? + //Region::RegionNodeInfo::DiseqList* del = d_regions[ d_regions_map[n] ]->d_nodes[n]->d_disequalities[0]; + //for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){ + // if( (*it).second ){ + // } + //} + //move node to region ri + d_regions[ri]->takeNode( d_regions[ d_regions_map[n] ], n ); + d_regions_map[n] = ri; +} + +int StrongSolverTheoryUf::ConflictFind::getNumDisequalitiesToRegion( Node n, int ri ){ + int ni = d_regions_map[n]; + int counter = 0; + Region::RegionNodeInfo::DiseqList* del = d_regions[ni]->d_nodes[n]->d_disequalities[0]; + for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){ + if( (*it).second ){ + if( d_regions_map[ (*it).first ]==ri ){ + counter++; + } + } + } + return counter; +} + +void StrongSolverTheoryUf::ConflictFind::getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq ){ + for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[ri]->d_nodes.begin(); + it != d_regions[ri]->d_nodes.end(); ++it ){ + if( it->second->d_valid ){ + Region::RegionNodeInfo::DiseqList* del = it->second->d_disequalities[0]; + for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){ + if( (*it2).second ){ + //if( !isValid( d_regions_map[ (*it2).first ] ) ){ + // Debug( "uf-ss-temp" ) << "^^^" << ri << " " << d_regions_map[ (*it2).first ].get() << std::endl; + // debugPrint( "uf-ss-temp" ); + //} + Assert( isValid( d_regions_map[ (*it2).first ] ) ); + //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl; + regions_diseq[ d_regions_map[ (*it2).first ] ]++; + } + } + } + } +} + +void StrongSolverTheoryUf::ConflictFind::explainClique( std::vector< Node >& clique, OutputChannel* out ){ + Assert( d_cardinality>0 ); + while( clique.size()>long(d_cardinality+1) ){ + clique.pop_back(); + } + //found a clique + Debug("uf-ss") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl; + Debug("uf-ss") << " "; + for( int i=0; i<(int)clique.size(); i++ ){ + Debug("uf-ss") << clique[i] << " "; + } + Debug("uf-ss") << std::endl; + Debug("uf-ss") << "Finding clique disequalities..." << std::endl; + std::vector< Node > conflict; + //collect disequalities, and nodes that must be equal within representatives + std::map< Node, std::map< Node, bool > > explained; + std::map< Node, std::map< Node, bool > > nodesWithinRep; + for( int i=0; i<(int)d_disequalities_index; i++ ){ + //if both sides of disequality exist in clique + Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] ); + Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] ); + if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) && + std::find( clique.begin(), clique.end(), r1 )!=clique.end() && + std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){ + explained[r1][r2] = true; + explained[r2][r1] = true; + conflict.push_back( d_disequalities[i] ); + nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true; + nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true; + if( conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) ){ + break; + } + } + } + //Debug("uf-ss") << conflict.size() << " " << clique.size() << std::endl; + Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) ); + //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 ); + Debug("uf-ss") << "Finding clique equalities internal to eq classes..." << std::endl; + //now, we must explain equalities within each equivalence class + for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){ + if( it->second.size()>1 ){ + Node prev; + //add explanation of t1 = t2 = ... = tn + for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + if( prev!=Node::null() ){ + //explain it2->first and prev + std::vector< TNode > expl; + d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl ); + for( int i=0; i<(int)expl.size(); i++ ){ + if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){ + conflict.push_back( expl[i] ); + } + } + } + prev = it2->first; + } + } + } + Debug("uf-ss") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl; + for( int i=0; i<(int)conflict.size(); i++ ){ + Debug("uf-ss") << conflict[i] << " "; + } + Debug("uf-ss") << std::endl; + //now, make the conflict + Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict ); + //add cardinality constraint + //Node cardNode = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_lemma_term, + // NodeManager::currentNM()->mkConst( Rational(d_cardinality) ) ); + Node cardNode = d_cardinality_literal[ d_cardinality ]; + conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() ); + Debug("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl; + //Notice() << "*** Add clique conflict " << conflictNode << std::endl; + out->lemma( conflictNode ); + ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas ); + + //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique. +} + +/** new node */ +void StrongSolverTheoryUf::ConflictFind::newEqClass( Node n ){ + if( d_regions_map.find( n )==d_regions_map.end() ){ + d_regions_map[n] = d_regions_index; + Debug("uf-ss") << "StrongSolverTheoryUf: New Eq Class " << n << std::endl; + Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl; + if( d_regions_index<d_regions.size() ){ + d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true); + d_regions[ d_regions_index ]->d_valid = true; + //Assert( d_regions[ d_regions_index ]->d_valid ); + Assert( d_regions[ d_regions_index ]->getNumReps()==0 ); + }else{ + d_regions.push_back( new Region( this, d_th->getSatContext() ) ); + } + d_regions[ d_regions_index ]->setRep( n, true ); + d_regions_index = d_regions_index + 1; + d_reps = d_reps + 1; + } +} + +/** merge */ +void StrongSolverTheoryUf::ConflictFind::merge( Node a, Node b ){ + //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) ); + //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) ); + Debug("uf-ss") << "StrongSolverTheoryUf: Merging " << a << " = " << b << "..." << std::endl; + if( a!=b ){ + Assert( d_regions_map.find( a )!=d_regions_map.end() ); + Assert( d_regions_map.find( b )!=d_regions_map.end() ); + int ai = d_regions_map[a]; + int bi = d_regions_map[b]; + Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; + if( ai!=bi ){ + if( d_regions[ai]->getNumReps()==1 ){ + combineRegions( bi, ai ); + d_regions[bi]->setEqual( a, b ); + checkRegion( bi ); + }else if( d_regions[bi]->getNumReps()==1 ){ + combineRegions( ai, bi ); + d_regions[ai]->setEqual( a, b ); + checkRegion( ai ); + }else{ + // either move a to d_regions[bi], or b to d_regions[ai] + int aex = d_regions[ai]->d_nodes[a]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( a, bi ); + int bex = d_regions[bi]->d_nodes[b]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( b, ai ); + //based on which would produce the fewest number of external disequalities + if( aex<bex ){ + moveNode( a, bi ); + d_regions[bi]->setEqual( a, b ); + }else{ + moveNode( b, ai ); + d_regions[ai]->setEqual( a, b ); + } + checkRegion( ai ); + checkRegion( bi ); + } + }else{ + d_regions[ai]->setEqual( a, b ); + checkRegion( ai ); + } + d_reps = d_reps - 1; + d_regions_map[b] = -1; + } + Debug("uf-ss") << "Done merge." << std::endl; +} + +/** assert terms are disequal */ +void StrongSolverTheoryUf::ConflictFind::assertDisequal( Node a, Node b, Node reason ){ + //if they are not already disequal + a = d_th->d_equalityEngine.getRepresentative( a ); + b = d_th->d_equalityEngine.getRepresentative( b ); + if( !d_th->d_equalityEngine.areDisequal( a, b, true ) ){ + Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl; + //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) || + // a!=reason[0][0] || b!=reason[0][1] ){ + // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl; + //} + Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." << std::endl; + //add to list of disequalities + if( d_disequalities_index<d_disequalities.size() ){ + d_disequalities[d_disequalities_index] = reason; + }else{ + d_disequalities.push_back( reason ); + } + d_disequalities_index = d_disequalities_index + 1; + //now, add disequalities to regions + Assert( d_regions_map.find( a )!=d_regions_map.end() ); + Assert( d_regions_map.find( b )!=d_regions_map.end() ); + int ai = d_regions_map[a]; + int bi = d_regions_map[b]; + Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; + if( ai==bi ){ + //internal disequality + d_regions[ai]->setDisequal( a, b, 1, true ); + d_regions[ai]->setDisequal( b, a, 1, true ); + }else{ + //external disequality + d_regions[ai]->setDisequal( a, b, 0, true ); + d_regions[bi]->setDisequal( b, a, 0, true ); + checkRegion( ai ); + checkRegion( bi ); + } + //Notice() << "done" << std::endl; + } +} + +void StrongSolverTheoryUf::ConflictFind::assertCardinality( int c, bool val ){ + Assert( d_cardinality_literal.find( c )!=d_cardinality_literal.end() ); + d_cardinality_assertions[ d_cardinality_literal[c] ] = val; + if( val ){ + d_hasCard = true; + } +} + +bool StrongSolverTheoryUf::ConflictFind::checkRegion( int ri, bool rec ){ + if( isValid(ri) ){ + Assert( d_cardinality>0 ); + //first check if region is in conflict + std::vector< Node > clique; + if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){ + //explain clique + explainClique( clique, &d_th->getOutputChannel() ); + return false; + }else if( d_regions[ri]->getMustCombine( d_cardinality ) ){ + //this region must merge with another + Debug("uf-ss-check-region") << "We must combine Region #" << ri << ". " << std::endl; + d_regions[ri]->debugPrint("uf-ss-check-region"); + ////alternatively, check if we can reduce the number of external disequalities by moving single nodes + //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){ + // if( it->second ){ + // int inDeg = d_regions[i]->d_disequalities_size[1][ it-> first ]; + // int outDeg = d_regions[i]->d_disequalities_size[1][ it-> first ]; + // if( inDeg<outDeg ){ + // } + // } + //} + //take region with maximum disequality density + double maxScore = 0; + int maxRegion = -1; + std::map< int, int > regions_diseq; + getDisequalitiesToRegions( ri, regions_diseq ); + for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){ + Debug("uf-ss-check-region") << it->first << " : " << it->second << std::endl; + } + for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){ + Assert( it->first!=ri ); + Assert( isValid( it->first ) ); + Assert( d_regions[ it->first ]->getNumReps()>0 ); + double tempScore = double(it->second)/double(d_regions[it->first]->getNumReps() ); + if( tempScore>maxScore ){ + maxRegion = it->first; + maxScore = tempScore; + } + } + Assert( maxRegion!=-1 ); + Debug("uf-ss-check-region") << "Combine with region #" << maxRegion << ":" << std::endl; + d_regions[maxRegion]->debugPrint("uf-ss-check-region"); + combineRegions( ri, maxRegion ); + if( rec ){ + checkRegion( ri, rec ); + } + //std::vector< Node > clique; + //if( d_regions[ri]->check( Theory::EFFORT_STANDARD, cardinality, clique ) ){ + // //explain clique + // Notice() << "found clique " << std::endl; + //} + return true; + } + } + return false; +} + +bool StrongSolverTheoryUf::ConflictFind::disambiguateTerms( OutputChannel* out ){ + Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl; + bool lemmaAdded = false; + //otherwise, determine ambiguous pairs of ground terms for relevant sorts + TermDb* db = d_th->getQuantifiersEngine()->getTermDatabase(); + for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){ + Debug("uf-ss-disamb") << "Check " << it->first << std::endl; + if( it->second.size()>1 ){ + if( StrongSolverTheoryUf::involvesRelevantType( it->second[0] ) ){ + for( int i=0; i<(int)it->second.size(); i++ ){ + for( int j=(i+1); j<(int)it->second.size(); j++ ){ + Kind knd = it->second[i].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL; + Node eq = NodeManager::currentNM()->mkNode( knd, it->second[i], it->second[j] ); + eq = Rewriter::rewrite(eq); + //determine if they are ambiguous + if( d_term_amb.find( eq )==d_term_amb.end() ){ + Debug("uf-ss-disamb") << "Check disambiguate " << it->second[i] << " " << it->second[j] << std::endl; + d_term_amb[ eq ] = true; + //if they are equal + if( d_th->d_equalityEngine.areEqual( it->second[i], it->second[j] ) ){ + d_term_amb[ eq ] = false; + }else{ + //if an argument is disequal, then they are not ambiguous + for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){ + if( d_th->d_equalityEngine.areDisequal( it->second[i][k], it->second[j][k], true ) ){ + d_term_amb[ eq ] = false; + break; + } + } + } + if( d_term_amb[ eq ] ){ + Debug("uf-ss-disamb") << "Disambiguate " << it->second[i] << " " << it->second[j] << std::endl; + //must add lemma + std::vector< Node > children; + children.push_back( eq ); + for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){ + Kind knd2 = it->second[i][k].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL; + Node eqc = NodeManager::currentNM()->mkNode( knd2, it->second[i][k], it->second[j][k] ); + children.push_back( eqc.notNode() ); + } + Assert( children.size()>1 ); + Node lem = NodeManager::currentNM()->mkNode( OR, children ); + Debug( "uf-ss-lemma" ) << "*** Diambiguate lemma : " << lem << std::endl; + //Notice() << "*** Diambiguate lemma : " << lem << std::endl; + out->lemma( lem ); + d_term_amb[ eq ] = false; + lemmaAdded = true; + ++( d_th->getStrongSolver()->d_statistics.d_disamb_term_lemmas ); + } + } + } + } + } + } + } + Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl; + return lemmaAdded; +} + +/** check */ +void StrongSolverTheoryUf::ConflictFind::check( Theory::Effort level, OutputChannel* out ){ + if( level>=Theory::EFFORT_STANDARD ){ + Assert( d_cardinality>0 ); + Debug("uf-ss") << "StrongSolverTheoryUf: Check " << level << " " << d_type << std::endl; + //Notice() << "StrongSolverTheoryUf: Check " << level << std::endl; + if( d_reps<=(unsigned)d_cardinality ){ + Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl; + if( level==Theory::EFFORT_FULL ){ + Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl; + //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl; + //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl; + //Notice() << cardinality << " "; + } + return; + }else{ + //do a check within each region + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + std::vector< Node > clique; + if( d_regions[i]->check( level, d_cardinality, clique ) ){ + //explain clique + explainClique( clique, out ); + return; + }else{ + Debug("uf-ss-debug") << "No clique in Region #" << i << std::endl; + } + } + } + if( level==Theory::EFFORT_FULL ){ + Debug("uf-ss-debug") << "Add splits?" << std::endl; + //see if we have any recommended splits + bool addedLemma = false; + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + if( d_regions[i]->hasSplits() ){ + d_regions[i]->addSplit( out ); + addedLemma = true; + ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas ); + } + } + } + if( !addedLemma ){ + Debug("uf-ss") << "No splits added." << std::endl; + if( Options::current()->fmfRegionSat ){ + //otherwise, try to disambiguate individual terms + if( !disambiguateTerms( out ) ){ + //no disequalities can be propagated + //we are in a situation where it suffices to apply a coloring to equivalence classes + //due to our invariants, we know no coloring conflicts will occur between regions, and thus + // we are SAT in this case. + Debug("uf-ss-sat") << "SAT: regions = " << getNumRegions() << std::endl; + //Notice() << "Model size for " << d_type << " is " << cardinality << ", regions = " << getNumRegions() << std::endl; + debugPrint("uf-ss-sat"); + } + }else{ + //naive strategy. combine the first two valid regions + int regIndex = -1; + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + if( regIndex==-1 ){ + regIndex = i; + }else{ + combineRegions( regIndex, i ); + check( level, out ); + } + } + } + } + } + } + } + } +} + +void StrongSolverTheoryUf::ConflictFind::propagate( Theory::Effort level, OutputChannel* out ){ + Assert( d_cardinality>0 ); + + //propagate the current cardinality as a decision literal + Node cn = d_cardinality_literal[ d_cardinality ]; + Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_type << ", cardinality = " << d_cardinality << std::endl; + Assert( !cn.isNull() ); + if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){ + out->propagateAsDecision( d_cardinality_literal[ d_cardinality ] ); + Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_cardinality_literal[ d_cardinality ]; + Debug("uf-ss-prop-as-dec") << " " << d_cardinality_literal[ d_cardinality ][0].getType() << std::endl; + } + +} + +void StrongSolverTheoryUf::ConflictFind::debugPrint( const char* c ){ + Debug( c ) << "-- Conflict Find:" << std::endl; + Debug( c ) << "Number of reps = " << d_reps << std::endl; + Debug( c ) << "Cardinality req = " << d_cardinality << std::endl; + unsigned debugReps = 0; + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + Debug( c ) << "Region #" << i << ": " << std::endl; + d_regions[i]->debugPrint( c, true ); + Debug( c ) << std::endl; + for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[i]->d_nodes.begin(); it != d_regions[i]->d_nodes.end(); ++it ){ + if( it->second->d_valid ){ + if( d_regions_map[ it->first ]!=i ){ + Debug( c ) << "***Bad regions map : " << it->first << " " << d_regions_map[ it->first ].get() << std::endl; + } + } + } + debugReps += d_regions[i]->getNumReps(); + } + } + if( debugReps!=d_reps ){ + Debug( c ) << "***Bad reps: " << d_reps << ", actual = " << debugReps << std::endl; + } +} + +int StrongSolverTheoryUf::ConflictFind::getNumRegions(){ + int count = 0; + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + count++; + } + } + return count; +} + +void StrongSolverTheoryUf::ConflictFind::setCardinality( int c, OutputChannel* out ){ + d_cardinality = c; + //add appropriate lemma + Node lem = getCardinalityLemma(); + out->lemma( lem ); + //add the appropriate lemma + Debug("uf-ss-fmf") << "Set cardinality " << d_type << " = " << c << std::endl; + Debug("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << std::endl; + out->propagateAsDecision( lem[0] ); + d_is_cardinality_requested = true; + d_is_cardinality_requested_c = true; + //now, require old literal to be decided false + //if( d_cardinality_literal.find( c-1 )!=d_cardinality_literal.end() ){ + // Debug("uf-ss-req-phase") << "Require phase " << d_cardinality_literal[c-1] << " = false " << std::endl; + // out->requirePhase( d_cardinality_literal[c-1], false ); + //} +} + +void StrongSolverTheoryUf::ConflictFind::getRepresentatives( std::vector< Node >& reps ){ + if( !Options::current()->fmfRegionSat ){ + bool foundRegion = false; + for( int i=0; i<(int)d_regions_index; i++ ){ + //should not have multiple regions at this point + if( foundRegion ){ + Assert( !d_regions[i]->d_valid ); + } + if( d_regions[i]->d_valid ){ + //this is the only valid region + d_regions[i]->getRepresentatives( reps ); + foundRegion = true; + } + } + }else{ + Unimplemented("Build representatives for fmf region sat is not implemented"); + } +} + +bool StrongSolverTheoryUf::ConflictFind::minimize( OutputChannel* out ){ + int validRegionIndex = -1; + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + if( validRegionIndex!=-1 ){ + combineRegions( validRegionIndex, i ); + if( !d_regions[validRegionIndex]->minimize( out ) ){ + return false; + } + }else{ + validRegionIndex = i; + } + } + } + if( !d_regions[validRegionIndex]->minimize( out ) ){ + return false; + } + return true; +} + + +Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){ + if( d_cardinality_lemma.find( d_cardinality )==d_cardinality_lemma.end() ){ + if( d_cardinality_lemma_term.isNull() ){ + std::stringstream ss; + ss << "fmf_term_" << d_type; + d_cardinality_lemma_term = NodeManager::currentNM()->mkVar( ss.str(), d_type ); + ModelBasisAttribute mba; + d_cardinality_lemma_term.setAttribute(mba,true); + } + Node lem = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_lemma_term, + NodeManager::currentNM()->mkConst( Rational( d_cardinality ) ) ); + lem = Rewriter::rewrite(lem); + d_cardinality_literal[ d_cardinality ] = lem; + lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); + d_cardinality_lemma[ d_cardinality ] = lem; + } + return d_cardinality_lemma[ d_cardinality ]; +} + +StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : +d_out( &out ), +d_th( th ), +d_conf_find_init( c ) +{ + +} + +/** new node */ +void StrongSolverTheoryUf::newEqClass( Node n ){ + TypeNode tn = n.getType(); + ConflictFind* c = getConflictFind( tn ); + if( c ){ + Debug("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl; + c->newEqClass( n ); + } + //else if( isRelevantType( tn ) ){ + // //Debug("uf-ss-solver") << "WAIT: StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl; + // //d_new_eq_class_waiting[tn].push_back( n ); + //} +} + +/** merge */ +void StrongSolverTheoryUf::merge( Node a, Node b ){ + TypeNode tn = a.getType(); + ConflictFind* c = getConflictFind( tn ); + if( c ){ + Debug("uf-ss-solver") << "StrongSolverTheoryUf: Merge " << a << " " << b << " " << tn << std::endl; + c->merge( a, b ); + } + //else if( isRelevantType( tn ) ){ + //} +} + +/** assert terms are disequal */ +void StrongSolverTheoryUf::assertDisequal( Node a, Node b, Node reason ){ + TypeNode tn = a.getType(); + ConflictFind* c = getConflictFind( tn ); + if( c ){ + Debug("uf-ss-solver") << "StrongSolverTheoryUf: Assert disequal " << a << " " << b << " " << tn << std::endl; + //Assert( d_th->d_equalityEngine.getRepresentative( a )==a ); + //Assert( d_th->d_equalityEngine.getRepresentative( b )==b ); + c->assertDisequal( a, b, reason ); + } + //else if( isRelevantType( tn ) ){ + //} +} + +/** assert a node */ +void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){ + Debug("uf-ss-assert") << "Assert " << n << " " << isDecision << std::endl; + if( n.getKind()==CARDINALITY_CONSTRAINT ){ + TypeNode tn = n[0].getType(); + Assert( d_conf_find[tn]->getCardinality()>0 ); + Assert( isRelevantType( tn ) ); + Assert( d_conf_find[tn] ); + long nCard = n[1].getConst<Rational>().getNumerator().getLong(); + d_conf_find[tn]->assertCardinality( nCard, true ); + if( nCard==d_conf_find[tn]->getCardinality() ){ + d_conf_find[tn]->d_is_cardinality_set = true; + d_conf_find[tn]->d_is_cardinality_requested = false; + d_conf_find[tn]->d_is_cardinality_requested_c = false; + } + }else if( n.getKind()==NOT && n[0].getKind()==CARDINALITY_CONSTRAINT ){ + //must add new lemma + Node nn = n[0]; + TypeNode tn = nn[0].getType(); + Assert( isRelevantType( tn ) ); + Assert( d_conf_find[tn] ); + long nCard = nn[1].getConst<Rational>().getNumerator().getLong(); + d_conf_find[tn]->assertCardinality( nCard, false ); + if( nCard==d_conf_find[tn]->getCardinality() ){ + AlwaysAssert(!isDecision, "Error: Negative cardinality node decided upon"); + Debug("uf-ss-fmf") << "No model of size " << d_conf_find[tn]->getCardinality() << " exists for type " << tn << std::endl; + //Notice() << "No model of size " << d_conf_find[tn]->getCardinality() << " exists for type " << tn << std::endl; + //increment to next cardinality + d_statistics.d_max_model_size.maxAssign( d_conf_find[tn]->getCardinality() + 1 ); + d_conf_find[tn]->setCardinality( d_conf_find[tn]->getCardinality() + 1, d_out ); + //Notice() << d_conf_find[tn]->getCardinality() << " "; + ////give up permanently on this cardinality + //d_out->lemma( n ); + } + }else{ + ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but + //// a theory propagation is not a decision. + //if( isDecision ){ + // for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){ + // if( !it->second->hasCardinalityAsserted() ){ + // Notice() << "Assert " << n << " " << isDecision << std::endl; + // Notice() << "Error: constraint asserted before cardinality for " << it->first << std::endl; + // Unimplemented(); + // } + // } + //} + } +} + + +/** check */ +void StrongSolverTheoryUf::check( Theory::Effort level ){ + Debug("uf-ss-solver") << "StrongSolverTheoryUf: check " << level << std::endl; + if( level==Theory::EFFORT_FULL ){ + debugPrint( "uf-ss-debug" ); + } + for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){ + it->second->check( level, d_out ); + } + Debug("uf-ss-solver") << "Done StrongSolverTheoryUf: check " << level << std::endl; +} + +/** propagate */ +void StrongSolverTheoryUf::propagate( Theory::Effort level ){ + for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){ + it->second->propagate( level, d_out ); + } +} + +void StrongSolverTheoryUf::preRegisterTerm( TNode n ){ + //shouldn't have to preregister this type (it may be that there are no quantifiers over tn) FIXME + TypeNode tn = n.getType(); + if( isRelevantType( tn ) ){ + preRegisterType( tn ); + } +} + +void StrongSolverTheoryUf::registerQuantifier( Node f ){ + Debug("uf-ss-register") << "Register quantifier " << f << std::endl; + //must ensure the quantifier does not quantify over arithmetic + for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ + TypeNode tn = f[0][i].getType(); + if( isRelevantType( tn ) ){ + preRegisterType( tn ); + }else{ + if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ + Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier"; + Debug("uf-ss-na") << " (" << f << ")"; + Debug("uf-ss-na") << std::endl; + Unimplemented("Cannot perform finite model finding on arithmetic quantifier"); + }else if( tn.isDatatype() ){ + Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier"; + Debug("uf-ss-na") << " (" << f << ")"; + Debug("uf-ss-na") << std::endl; + Unimplemented("Cannot perform finite model finding on datatype quantifier"); + } + } + } +} + +void StrongSolverTheoryUf::preRegisterType( TypeNode tn ){ + if( d_conf_find.find( tn )==d_conf_find.end() ){ + Debug("uf-ss-register") << "Preregister " << tn << "." << std::endl; + //enter into incremental finite model finding mode: try cardinality = 1 first + //if( !d_conf_types.empty() ){ + // Debug("uf-ss-na") << "Strong solver unimplemented for multiple sorts." << std::endl; + // Unimplemented(); + //} + d_conf_find[tn] = new ConflictFind( tn, d_th->getSatContext(), d_th ); + //assign cardinality restriction + d_statistics.d_max_model_size.maxAssign( 1 ); + d_conf_find[tn]->setCardinality( 1, d_out ); + ////add waiting equivalence classes now + //if( !d_new_eq_class_waiting[tn].empty() ){ + // Debug("uf-ss-register") << "Add " << (int)d_new_eq_class_waiting[tn].size() << " new eq classes." << std::endl; + // for( int i=0; i<(int)d_new_eq_class_waiting[tn].size(); i++ ){ + // newEqClass( d_new_eq_class_waiting[tn][i] ); + // } + // d_new_eq_class_waiting[tn].clear(); + //} + d_conf_types.push_back( tn ); + } +} + +StrongSolverTheoryUf::ConflictFind* StrongSolverTheoryUf::getConflictFind( TypeNode tn ){ + std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.find( tn ); + //pre-register the type if not done already + if( it==d_conf_find.end() ){ + if( isRelevantType( tn ) ){ + preRegisterType( tn ); + it = d_conf_find.find( tn ); + } + } + if( it!=d_conf_find.end() ){ + //initialize the type if necessary + if( d_conf_find_init.find( tn )==d_conf_find_init.end() ){ + //assign cardinality restriction + d_statistics.d_max_model_size.maxAssign( 1 ); + it->second->setCardinality( 1, d_out ); + d_conf_find_init[tn] = true; + } + return it->second; + }else{ + return NULL; + } +} + +void StrongSolverTheoryUf::notifyRestart(){ + Debug("uf-ss-prop-as-dec") << "Restart?" << std::endl; +} + +/** get cardinality for sort */ +int StrongSolverTheoryUf::getCardinality( TypeNode t ) { + ConflictFind* c = getConflictFind( t ); + if( c ){ + return c->getCardinality(); + }else{ + return -1; + } +} + +void StrongSolverTheoryUf::getRepresentatives( TypeNode t, std::vector< Node >& reps ){ + ConflictFind* c = getConflictFind( t ); + if( c ){ + c->getRepresentatives( reps ); + } +} + +Node StrongSolverTheoryUf::getCardinalityTerm( TypeNode t ){ + ConflictFind* c = getConflictFind( t ); + if( c ){ + return c->getCardinalityTerm(); + }else{ + return Node::null(); + } +} + +bool StrongSolverTheoryUf::minimize(){ + for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){ + if( !it->second->minimize( d_out ) ){ + return false; + } + } + return true; +} + +//print debug +void StrongSolverTheoryUf::debugPrint( const char* c ){ + //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine ); + //while( !eqc_iter.isFinished() ){ + // Debug( c ) << "Eq class [[" << (*eqc_iter) << "]]" << std::endl; + // EqClassIterator< TheoryUF::NotifyClass > eqc_iter2( *eqc_iter, &((TheoryUF*)d_th)->d_equalityEngine ); + // Debug( c ) << " "; + // while( !eqc_iter2.isFinished() ){ + // Debug( c ) << "[" << (*eqc_iter2) << "] "; + // eqc_iter2++; + // } + // Debug( c ) << std::endl; + // eqc_iter++; + //} + + for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){ + Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl; + it->second->debugPrint( c ); + Debug( c ) << std::endl; + } +} + +StrongSolverTheoryUf::Statistics::Statistics(): + d_clique_lemmas("StrongSolverTheoryUf::Clique_Lemmas", 0), + d_split_lemmas("StrongSolverTheoryUf::Split_Lemmas", 0), + d_disamb_term_lemmas("StrongSolverTheoryUf::Disambiguate_Term_Lemmas", 0), + d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 0) +{ + StatisticsRegistry::registerStat(&d_clique_lemmas); + StatisticsRegistry::registerStat(&d_split_lemmas); + StatisticsRegistry::registerStat(&d_disamb_term_lemmas); + StatisticsRegistry::registerStat(&d_max_model_size); +} + +StrongSolverTheoryUf::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_clique_lemmas); + StatisticsRegistry::unregisterStat(&d_split_lemmas); + StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas); + StatisticsRegistry::unregisterStat(&d_max_model_size); +} + +bool StrongSolverTheoryUf::isRelevantType( TypeNode t ){ + return t!=NodeManager::currentNM()->booleanType() && + t!=NodeManager::currentNM()->integerType() && + t!=NodeManager::currentNM()->realType() && + t!=NodeManager::currentNM()->builtinOperatorType() && + !t.isFunction() && + !t.isDatatype(); +} + +bool StrongSolverTheoryUf::involvesRelevantType( Node n ){ + if( n.getKind()==APPLY_UF ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( isRelevantType( n[i].getType() ) ){ + return true; + } + } + } + return false; +} diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h new file mode 100644 index 000000000..e36441f6d --- /dev/null +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -0,0 +1,322 @@ +/********************* */ +/*! \file theory_uf_strong_solver.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory uf strong solver + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H +#define __CVC4__THEORY_UF_STRONG_SOLVER_H + +#include "theory/theory.h" + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.h" + +#include "util/stats.h" + +namespace CVC4 { +namespace theory { + +struct ModelBasisAttributeId {}; +typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; + +namespace uf { + +class TheoryUF; + +class StrongSolverTheoryUf{ +protected: + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDChunkList<Node> NodeList; + typedef context::CDList<bool> BoolList; + typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap; +public: + /** information for incremental conflict/clique finding for a particular sort */ + class ConflictFind { + public: + /** a partition of the current equality graph for which cliques can occur internally */ + class Region { + public: + /** conflict find pointer */ + ConflictFind* d_cf; + /** information stored about each node in region */ + class RegionNodeInfo { + public: + /** disequality list for node */ + class DiseqList { + public: + DiseqList( context::Context* c ) : d_size( c, 0 ), d_disequalities( c ){} + ~DiseqList(){} + context::CDO< unsigned > d_size; + NodeBoolMap d_disequalities; + void setDisequal( Node n, bool valid ){ + Assert( d_disequalities.find( n )==d_disequalities.end() || d_disequalities[n]!=valid ); + d_disequalities[ n ] = valid; + d_size = d_size + ( valid ? 1 : -1 ); + } + }; + private: + DiseqList d_internal; + DiseqList d_external; + public: + /** constructor */ + RegionNodeInfo( context::Context* c ) : d_internal( c ), d_external( c ), d_valid( c, true ){ + d_disequalities[0] = &d_internal; + d_disequalities[1] = &d_external; + } + ~RegionNodeInfo(){} + context::CDO< bool > d_valid; + DiseqList* d_disequalities[2]; + + int getNumDisequalities() { return d_disequalities[0]->d_size + d_disequalities[1]->d_size; } + int getNumExternalDisequalities() { return d_disequalities[0]->d_size; } + int getNumInternalDisequalities() { return d_disequalities[1]->d_size; } + }; + ///** end class RegionNodeInfo */ + private: + //a postulated clique + NodeBoolMap d_testClique; + context::CDO< unsigned > d_testCliqueSize; + //disequalities needed for this clique to happen + NodeBoolMap d_splits; + context::CDO< unsigned > d_splitsSize; + /** get split */ + Node getBestSplit(); + private: + //number of valid representatives in this region + context::CDO< unsigned > d_reps_size; + //total disequality size (external) + context::CDO< unsigned > d_total_diseq_external; + //total disequality size (internal) + context::CDO< unsigned > d_total_diseq_internal; + public: + //constructor + Region( ConflictFind* cf, context::Context* c ) : d_cf( cf ), d_testClique( c ), d_testCliqueSize( c, 0 ), + d_splits( c ), d_splitsSize( c, 0 ), d_reps_size( c, 0 ), d_total_diseq_external( c, 0 ), + d_total_diseq_internal( c, 0 ), d_valid( c, true ) { + } + ~Region(){} + //region node infomation + std::map< Node, RegionNodeInfo* > d_nodes; + //whether region is valid + context::CDO< bool > d_valid; + public: + //get num reps + int getNumReps() { return d_reps_size; } + // has representative + bool hasRep( Node n ) { return d_nodes.find( n )!=d_nodes.end() && d_nodes[n]->d_valid; } + //take node from region + void takeNode( Region* r, Node n ); + //merge with other region + void combine( Region* r ); + /** set rep */ + void setRep( Node n, bool valid ); + /** merge */ + void setEqual( Node a, Node b ); + //set n1 != n2 to value 'valid', type is whether it is internal/external + void setDisequal( Node n1, Node n2, int type, bool valid ); + // is disequal + bool isDisequal( Node n1, Node n2, int type ); + public: + /** get must merge */ + bool getMustCombine( int cardinality ); + /** check for cliques */ + bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique ); + /** has splits */ + bool hasSplits() { return d_splitsSize>0; } + /** add split */ + void addSplit( OutputChannel* out ); + /** get representatives */ + void getRepresentatives( std::vector< Node >& reps ); + /** minimize */ + bool minimize( OutputChannel* out ); + /** get external disequalities */ + void getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ); + //print debug + void debugPrint( const char* c, bool incClique = false ); + }; + private: + /** theory uf pointer */ + TheoryUF* d_th; + /** regions used to d_region_index */ + context::CDO< unsigned > d_regions_index; + /** vector of regions */ + std::vector< Region* > d_regions; + /** map from Nodes to index of d_regions they exist in, -1 means invalid */ + NodeIntMap d_regions_map; + /** regions used to d_region_index */ + context::CDO< unsigned > d_disequalities_index; + /** list of all disequalities */ + std::vector< Node > d_disequalities; + /** number of representatives in all regions */ + context::CDO< unsigned > d_reps; + /** whether two terms are ambiguous (indexed by equalities) */ + NodeBoolMap d_term_amb; + private: + /** merge regions */ + void combineRegions( int ai, int bi ); + /** move node n to region ri */ + void moveNode( Node n, int ri ); + /** get number of disequalities from node n to region ri */ + int getNumDisequalitiesToRegion( Node n, int ri ); + /** get number of disequalities from Region r to other regions */ + void getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq ); + /** check if we need to combine region ri */ + bool checkRegion( int ri, bool rec = true ); + /** explain clique */ + void explainClique( std::vector< Node >& clique, OutputChannel* out ); + /** is valid */ + bool isValid( int ri ) { return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->d_valid; } + /** check ambiguous terms */ + bool disambiguateTerms( OutputChannel* out ); + private: + /** cardinality operating with */ + context::CDO< int > d_cardinality; + /** type */ + TypeNode d_type; + /** cardinality lemma term */ + Node d_cardinality_lemma_term; + /** cardinality literals */ + std::map< int, Node > d_cardinality_literal; + /** cardinality lemmas */ + std::map< int, Node > d_cardinality_lemma; + /** cardinality assertions (indexed by cardinality literals ) */ + NodeBoolMap d_cardinality_assertions; + public: + ConflictFind( TypeNode tn, context::Context* c, TheoryUF* th ) : + d_th( th ), d_regions_index( c, 0 ), d_regions_map( c ), d_disequalities_index( c, 0 ), + d_reps( c, 0 ), d_term_amb( c ), d_cardinality( c, 1 ), d_type( tn ), + d_cardinality_assertions( c ), d_is_cardinality_set( c, false ), + d_is_cardinality_requested_c( c, false ), d_is_cardinality_requested( false ), d_hasCard( c, false ){} + ~ConflictFind(){} + /** new node */ + void newEqClass( Node n ); + /** merge */ + void merge( Node a, Node b ); + /** assert terms are disequal */ + void assertDisequal( Node a, Node b, Node reason ); + /** assert cardinality */ + void assertCardinality( int c, bool val ); + /** whether cardinality has been asserted */ + bool hasCardinalityAsserted() { return d_hasCard; } + /** check */ + void check( Theory::Effort level, OutputChannel* out ); + /** propagate */ + void propagate( Theory::Effort level, OutputChannel* out ); + //print debug + void debugPrint( const char* c ); + /** set cardinality */ + void setCardinality( int c, OutputChannel* out ); + /** get cardinality */ + int getCardinality() { return d_cardinality; } + /** get representatives */ + void getRepresentatives( std::vector< Node >& reps ); + /** get model basis term */ + Node getCardinalityTerm() { return d_cardinality_lemma_term; } + /** minimize */ + bool minimize( OutputChannel* out ); + /** get cardinality lemma */ + Node getCardinalityLemma(); + public: + /** get number of regions (for debugging) */ + int getNumRegions(); + /** is cardinality set */ + context::CDO< bool > d_is_cardinality_set; + context::CDO< bool > d_is_cardinality_requested_c; + bool d_is_cardinality_requested; + /** whether a positive cardinality constraint has been asserted */ + context::CDO< bool > d_hasCard; + }; /** class ConflictFind */ +private: + /** The output channel for the strong solver. */ + OutputChannel* d_out; + /** theory uf pointer */ + TheoryUF* d_th; + /** conflict find structure, one for each type */ + std::map< TypeNode, ConflictFind* > d_conf_find; + /** all types */ + std::vector< TypeNode > d_conf_types; + /** whether conflict find data structures have been initialized */ + TypeNodeBoolMap d_conf_find_init; + /** pre register type */ + void preRegisterType( TypeNode tn ); + /** get conflict find */ + ConflictFind* getConflictFind( TypeNode tn ); +public: + StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th); + ~StrongSolverTheoryUf() {} + /** new node */ + void newEqClass( Node n ); + /** merge */ + void merge( Node a, Node b ); + /** assert terms are disequal */ + void assertDisequal( Node a, Node b, Node reason ); + /** assert node */ + void assertNode( Node n, bool isDecision ); +public: + /** check */ + void check( Theory::Effort level ); + /** propagate */ + void propagate( Theory::Effort level ); + /** preregister a term */ + void preRegisterTerm( TNode n ); + /** preregister a quantifier */ + void registerQuantifier( Node f ); + /** notify restart */ + void notifyRestart(); +public: + /** identify */ + std::string identify() const { return std::string("StrongSolverTheoryUf"); } + //print debug + void debugPrint( const char* c ); +public: + /** get number of types */ + int getNumCardinalityTypes() { return (int)d_conf_types.size(); } + /** get type */ + TypeNode getCardinalityType( int i ) { return d_conf_types[i]; } + /** get cardinality for sort */ + int getCardinality( TypeNode t ); + /** get representatives */ + void getRepresentatives( TypeNode t, std::vector< Node >& reps ); + /** get cardinality term */ + Node getCardinalityTerm( TypeNode t ); + /** minimize */ + bool minimize(); + + class Statistics { + public: + IntStat d_clique_lemmas; + IntStat d_split_lemmas; + IntStat d_disamb_term_lemmas; + IntStat d_max_model_size; + Statistics(); + ~Statistics(); + }; + /** statistics class */ + Statistics d_statistics; + + /** is relavant type */ + static bool isRelevantType( TypeNode t ); + /** involves relavant type */ + static bool involvesRelevantType( Node n ); +};/* class StrongSolverTheoryUf */ + +} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY_UF_STRONG_SOLVER_H */ diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 3d7e51746..b68a11abd 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -59,6 +59,20 @@ public: } };/* class UfTypeRule */ +class CardinalityConstraintTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + if( check ) { + TypeNode valType = n[1].getType(check); + if( valType != nodeManager->integerType() ) { + throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be integer"); + } + } + return nodeManager->booleanType(); + } +};/* class UfTypeRule */ + }/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |