diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.h | 38 | ||||
-rw-r--r-- | src/theory/uf/kinds | 45 | ||||
-rw-r--r-- | src/theory/uf/options | 18 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 73 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 75 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.h | 18 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 1556 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 230 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 62 |
10 files changed, 1263 insertions, 856 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 1e3b276a4..45d1b4acf 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -82,7 +82,7 @@ public: virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0; /** - * Notifies about the merge of two constant terms. After this, all work is suspended and all you + * Notifies about the merge of two constant terms. After this, all work is suspended and all you * can do is ask for explanations. * * @param t1 a constant term @@ -384,7 +384,7 @@ private: std::vector<TriggerId> d_nodeTriggers; /** - * Map from ids to whether they are constants (constants are always + * Map from ids to whether they are constants (constants are always * representatives of their class. */ std::vector<bool> d_isConstant; @@ -427,7 +427,7 @@ private: /** * Get an explanation of the equality t1 = t2. Returns the asserted equalities that * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere - * else. + * else. */ void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const; @@ -440,7 +440,7 @@ private: Node d_true; /** True node id */ EqualityNodeId d_trueId; - + /** The false node */ Node d_false; /** False node id */ @@ -484,12 +484,12 @@ private: /** Internal tags for creating a new set */ Theory::Set d_newSetTags; - + /** Internal triggers for creating a new set */ EqualityNodeId d_newSetTriggers[THEORY_LAST]; - + /** Size of the internal triggers array */ - unsigned d_newSetTriggersSize; + unsigned d_newSetTriggersSize; /** The information about trigger terms is stored in this easily maintained memory. */ char* d_triggerDatabase; @@ -524,7 +524,7 @@ private: struct TriggerSetUpdate { EqualityNodeId classId; TriggerTermSetRef oldValue; - TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id) + TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id) : classId(classId), oldValue(oldValue) {} };/* struct EqualityEngine::TriggerSetUpdate */ @@ -591,7 +591,7 @@ private: * reasons should be pushed on the reasons vector. */ void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId); - + /** * An equality tagged with a set of tags. */ @@ -599,10 +599,10 @@ private: /** Id of the equality */ EqualityNodeId equalityId; /** TriggerSet reference for the class of one of the sides */ - TriggerTermSetRef triggerSetRef; + TriggerTermSetRef triggerSetRef; /** Is trigger equivalent to the lhs (rhs otherwise) */ bool lhs; - + TaggedEquality(EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = true) : equalityId(equalityId), triggerSetRef(triggerSetRef), lhs(lhs) {} }; @@ -625,9 +625,9 @@ private: /** * Propagates the remembered disequalities with given tags the original triggers for those tags, - * and the set of disequalities produced by above. + * and the set of disequalities produced by above. */ - bool propagateTriggerTermDisequalities(Theory::Set tags, + bool propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify); /** Name of the equality engine */ @@ -636,12 +636,12 @@ private: public: /** - * Initialize the equality engine, given the notification class. + * Initialize the equality engine, given the notification class. */ EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name); /** - * Initialize the equality engine with no notification class. + * Initialize the equality engine with no notification class. */ EqualityEngine(context::Context* context, std::string name); @@ -791,7 +791,7 @@ class EqClassesIterator { const eq::EqualityEngine* d_ee; size_t d_it; - + std::vector< Node > d_visited; public: EqClassesIterator(): d_ee(NULL), d_it(0){ } @@ -812,11 +812,11 @@ public: return !(*this == i); } EqClassesIterator& operator++() { - Node orig = d_ee->d_nodes[d_it]; + d_visited.push_back( 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_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it] || + std::find( d_visited.begin(), d_visited.end(), d_ee->d_nodes[d_it] )!=d_visited.end() ) ) { // this line is necessary for ignoring duplicates ++d_it; } return *this; diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index efad8beb9..1d179248c 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -9,7 +9,7 @@ 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 ppStaticLearn presolve +properties check propagate ppStaticLearn presolve getNextDecisionRequest rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" @@ -19,47 +19,4 @@ typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule operator CARDINALITY_CONSTRAINT 2 "cardinality constraint" typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule -# -# For compact function models -# There are three cases for FUNCTION_MODEL nodes: -# (1) The node has two children, the first being of kind FUNCTION_CASE_SPLIT. The second child specifies a default value. -# (2) The node has one child of kind FUNCTION_CASE_SPLIT. -# (3) The node has one child, it's default value. -# -# Semantics of FUNCTION_MODEL kind-ed nodes. The value of n applied to arguments args is -# -# getValueFM( n, args, 0 ), where: -# -# Node getValueFM( n, args, argIndex ) -# if n.getKind()!=FUNCTION_MODEL -# return n; -# else if (1) -# val = getValueFCS( n[0], args, argIndex ); -# if !val.isNull() -# return val; -# else -# return getValueFM( n[1], args, argIndex+1 ); -# else if (2) -# return getValueFCS( n[0], args, argIndex ); -# else if (3) -# return getValueFM( n[0], args, argIndex+1 ); -# -# Node getValueFCS( n, args, argIndex ) : -# //n.getKind()==FUNCTION_CASE_SPLIT -# //n[j].getKind()==FUNCTION_CASE for all 0<=j<n.getNumChildren() -# if( args[argIndex]=n[i][0] for some i) -# return getValueFM( n[i][1], args, argIndex+1 ); -# else -# return null; -# - -operator FUNCTION_MODEL 1:2 "function model" -typerule FUNCTION_MODEL ::CVC4::theory::uf::FunctionModelTypeRule - -operator FUNCTION_CASE_SPLIT 1: "function case split" -typerule FUNCTION_CASE_SPLIT ::CVC4::theory::uf::FunctionCaseSplitTypeRule - -operator FUNCTION_CASE 2 "function case" -typerule FUNCTION_CASE ::CVC4::theory::uf::FunctionCaseTypeRule - endtheory diff --git a/src/theory/uf/options b/src/theory/uf/options index 6f6900da0..8185f0b3d 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -9,4 +9,22 @@ option ufSymmetryBreaker uf-symmetry-breaker --enable-symmetry-breaker/--disable use UF symmetry breaker (Deharbe et al., CADE 2011) /turns off UF symmetry breaker (Deharbe et al., CADE 2011) +option ufssRegions /--disable-uf-ss-regions bool :default true + disable region-based method for discovering cliques and splits in uf strong solver +option ufssEagerSplits --uf-ss-eager-split bool :default false + add splits eagerly for uf strong solver +option ufssColoringSat --uf-ss-coloring-sat bool :default false + use coloring-based SAT heuristic for uf strong solver +option ufssTotality --uf-ss-totality bool :default false + use totality axioms for enforcing cardinality constraints +option ufssTotalityLazy --uf-ss-totality-lazy bool :default false + apply totality axioms lazily +option ufssAbortCardinality --uf-ss-abort-card=N int :default -1 + tells the uf strong solver a cardinality to abort at (-1 == no limit, default) +option ufssSmartSplits --uf-ss-smart-split bool :default false + use smart splitting heuristic for uf strong solver +option ufssModelInference --uf-ss-model-infer bool :default false + use model inference method for uf strong solver + + endmodule diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 5b8470567..a1500e084 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -23,6 +23,7 @@ #include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/model.h" +#include "theory/type_enumerator.h" using namespace std; using namespace CVC4; @@ -80,6 +81,10 @@ void TheoryUF::check(Effort level) { if (d_thss != NULL) { bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); d_thss->assertNode(fact, isDecision); + if( d_thss->isConflict() ){ + d_conflict = true; + return; + } } // Do the work @@ -98,6 +103,9 @@ void TheoryUF::check(Effort level) { if (d_thss != NULL) { if (! d_conflict) { d_thss->check(level); + if( d_thss->isConflict() ){ + d_conflict = true; + } } } @@ -127,6 +135,9 @@ void TheoryUF::preRegisterTerm(TNode node) { // Remember the function and predicate terms d_functionsTerms.push_back(node); break; + case kind::CARDINALITY_CONSTRAINT: + //do nothing + break; default: // Variables etc d_equalityEngine.addTerm(node); @@ -150,8 +161,16 @@ bool TheoryUF::propagate(TNode literal) { }/* TheoryUF::propagate(TNode) */ void TheoryUF::propagate(Effort effort) { - if (d_thss != NULL) { - return d_thss->propagate(effort); + //if (d_thss != NULL) { + // return d_thss->propagate(effort); + //} +} + +Node TheoryUF::getNextDecisionRequest(){ + if (d_thss != NULL && !d_conflict) { + return d_thss->getNextDecisionRequest(); + }else{ + return Node::null(); } } @@ -173,8 +192,55 @@ Node TheoryUF::explain(TNode literal) { return mkAnd(assumptions); } -void TheoryUF::collectModelInfo( TheoryModel* m ){ +void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); + if( fullModel ){ +#if 1 + std::map< TypeNode, int > type_count; + //must choose proper representatives + // for each equivalence class, specify the constructor as a representative + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + TypeNode tn = eqc.getType(); + if( tn.isSort() ){ + if( type_count.find( tn )==type_count.end() ){ + type_count[tn] = 0; + } + std::stringstream ss; + ss << Expr::setlanguage(options::outputLanguage()); + ss << "$t_" << tn << (type_count[tn]+1); + type_count[tn]++; + Node rep = NodeManager::currentNM()->mkSkolem( ss.str(), tn ); + Trace("mkVar") << "TheoryUF::collectModelInfo: make variable " << rep << " : " << tn << std::endl; + //specify the constant as the representative + m->assertEquality( eqc, rep, true ); + m->assertRepresentative( rep ); + } + ++eqcs_i; + } +#else + std::map< TypeNode, TypeEnumerator* > type_enums; + //must choose proper representatives + // for each equivalence class, specify the constructor as a representative + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + TypeNode tn = eqc.getType(); + if( tn.isSort() ){ + if( type_enums.find( tn )==type_enums.end() ){ + type_enums[tn] = new TypeEnumerator( tn ); + } + Node rep = *(*type_enums[tn]); + ++(*type_enums[tn]); + //specify the constant as the representative + m->assertEquality( eqc, rep, true ); + m->assertRepresentative( rep ); + } + ++eqcs_i; + } + #endif + } } void TheoryUF::presolve() { @@ -481,3 +547,4 @@ Node TheoryUF::ppRewrite(TNode node) { } } } + diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 604b1f44c..62ca640aa 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -193,7 +193,7 @@ public: void preRegisterTerm(TNode term); Node explain(TNode n); - void collectModelInfo( TheoryModel* m ); + void collectModelInfo( TheoryModel* m, bool fullModel ); void ppStaticLearn(TNode in, NodeBuilder<>& learned); void presolve(); @@ -202,6 +202,7 @@ public: void computeCareGraph(); void propagate(Effort effort); + Node getNextDecisionRequest(); EqualityStatus getEqualityStatus(TNode a, TNode b); @@ -226,7 +227,6 @@ public: 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_model.cpp b/src/theory/uf/theory_uf_model.cpp index 0082f4840..b8110a2aa 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -136,35 +136,46 @@ Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& inde } } -Node UfModelTreeNode::getFunctionValue(){ +Node UfModelTreeNode::getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue ){ if( !d_data.empty() ){ - Node defaultValue; + Node defaultValue = argDefaultValue; + if( d_data.find( Node::null() )!=d_data.end() ){ + defaultValue = d_data[Node::null()].getFunctionValue( args, index+1, argDefaultValue ); + } std::vector< Node > caseValues; + std::map< Node, Node > caseArg; for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - if( it->first.isNull() ){ - defaultValue = it->second.getFunctionValue(); - }else{ - caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) ); + if( !it->first.isNull() ){ + Node val = it->second.getFunctionValue( args, index+1, defaultValue ); + caseValues.push_back( val ); + caseArg[ val ] = it->first; } } - if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){ - return defaultValue; - }else{ - std::vector< Node > children; - if( !caseValues.empty() ){ - children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) ); - } - if( !defaultValue.isNull() ){ - children.push_back( defaultValue ); - } - return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children ); + Node retNode = defaultValue; + for( int i=((int)caseValues.size()-1); i>=0; i-- ){ + retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( caseArg[ caseValues[i] ] ), caseValues[i], retNode ); } + return retNode; }else{ Assert( !d_value.isNull() ); return d_value; } } +//update function +void UfModelTreeNode::update( TheoryModel* m ){ + if( !d_value.isNull() ){ + d_value = m->getRepresentative( d_value ); + } + std::map< Node, UfModelTreeNode > old = d_data; + d_data.clear(); + for( std::map< Node, UfModelTreeNode >::iterator it = old.begin(); it != old.end(); ++it ){ + Node rep = m->getRepresentative( it->first ); + d_data[ rep ] = it->second; + d_data[ rep ].update( m ); + } +} + //simplify function void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){ if( argIndex<(int)op.getType().getNumChildren()-1 ){ @@ -251,31 +262,17 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector } } - -Node UfModelTree::toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ){ - if( fm_node.getKind()==FUNCTION_MODEL ){ - if( fm_node[0].getKind()==FUNCTION_CASE_SPLIT ){ - Node retNode; - Node childDefaultNode = defaultNode; - //get new default - if( fm_node.getNumChildren()==2 ){ - childDefaultNode = toIte2( fm_node[1], args, index+1, defaultNode ); - } - retNode = childDefaultNode; - for( int i=(int)fm_node[0].getNumChildren()-1; i>=0; i-- ){ - Node childNode = toIte2( fm_node[0][1], args, index+1, childDefaultNode ); - retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( fm_node[0][0] ), childNode, retNode ); - } - return retNode; - }else{ - return toIte2( fm_node[0], args, index+1, defaultNode ); - } - }else{ - return fm_node; +Node UfModelTree::getFunctionValue( const char* argPrefix ){ + TypeNode type = d_op.getType(); + std::vector< Node > vars; + for( size_t i=0; i<type.getNumChildren()-1; i++ ){ + std::stringstream ss; + ss << argPrefix << (i+1); + vars.push_back( NodeManager::currentNM()->mkSkolem( ss.str(), type[i] ) ); } + return getFunctionValue( vars ); } - Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){ //Notice() << "Get intersection " << n1 << " " << n2 << std::endl; isGround = true; diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 9dba16608..61c0714a3 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -48,7 +48,9 @@ public: /** getConstant Value function */ Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ); /** getFunctionValue */ - Node getFunctionValue(); + Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue ); + /** update function */ + void update( TheoryModel* m ); /** simplify function */ void simplify( Node op, Node defaultVal, int argIndex ); /** is total ? */ @@ -123,12 +125,15 @@ public: return d_tree.getConstantValue( m, n, d_index_order, 0 ); } /** getFunctionValue - * Returns a compact representation of this function, of kind FUNCTION_MODEL. - * See documentation in theory/uf/kinds + * Returns a representation of this function. */ - Node getFunctionValue(){ - return d_tree.getFunctionValue(); - } + Node getFunctionValue( std::vector< Node >& args ){ return d_tree.getFunctionValue( args, 0, Node::null() ); } + /** getFunctionValue for args with set prefix */ + Node getFunctionValue( const char* argPrefix ); + /** update + * This will update all values in the tree to be representatives in m. + */ + void update( TheoryModel* m ){ d_tree.update( m ); } /** simplify the tree */ void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); } /** is this tree total? */ @@ -147,6 +152,7 @@ private: public: /** to ITE function for function model nodes */ static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); } + static Node toIte( TypeNode type, Node fm_node, const char* argPrefix ); }; class UfModelTreeGenerator diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index f0b386cae..47c51d8b9 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -19,10 +19,9 @@ #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf_instantiator.h" #include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/uf/options.h" -//#define USE_SMART_SPLITS //#define ONE_SPLIT_REGION //#define DISABLE_QUICK_CLIQUE_CHECKS //#define COMBINE_REGIONS_SMALL_INTO_LARGE @@ -34,16 +33,11 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; -void StrongSolverTheoryUf::ConflictFind::Region::addRep( Node n ) { +void StrongSolverTheoryUf::SortRepModel::Region::addRep( Node n ) { setRep( n, true ); } -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"); +void StrongSolverTheoryUf::SortRepModel::Region::takeNode( StrongSolverTheoryUf::SortRepModel::Region* r, Node n ){ Assert( !hasRep( n ) ); Assert( r->hasRep( n ) ); //add representative @@ -75,7 +69,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::takeNode( StrongSolverTheoryUf: r->setRep( n, false ); } -void StrongSolverTheoryUf::ConflictFind::Region::combine( StrongSolverTheoryUf::ConflictFind::Region* r ){ +void StrongSolverTheoryUf::SortRepModel::Region::combine( StrongSolverTheoryUf::SortRepModel::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 ){ @@ -107,7 +101,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::combine( StrongSolverTheoryUf:: } /** setEqual */ -void StrongSolverTheoryUf::ConflictFind::Region::setEqual( Node a, Node b ){ +void StrongSolverTheoryUf::SortRepModel::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++ ){ @@ -129,7 +123,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::setEqual( Node a, Node b ){ setRep( b, false ); } -void StrongSolverTheoryUf::ConflictFind::Region::setDisequal( Node n1, Node n2, int type, bool valid ){ +void StrongSolverTheoryUf::SortRepModel::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 ); @@ -155,7 +149,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::setDisequal( Node n1, Node n2, } } -void StrongSolverTheoryUf::ConflictFind::Region::setRep( Node n, bool valid ){ +void StrongSolverTheoryUf::SortRepModel::Region::setRep( Node n, bool valid ){ Assert( hasRep( n )!=valid ); if( valid && d_nodes.find( n )==d_nodes.end() ){ d_nodes[n] = new RegionNodeInfo( d_cf->d_th->getSatContext() ); @@ -179,22 +173,24 @@ void StrongSolverTheoryUf::ConflictFind::Region::setRep( Node n, bool valid ){ } } -bool StrongSolverTheoryUf::ConflictFind::Region::isDisequal( Node n1, Node n2, int type ){ +bool StrongSolverTheoryUf::SortRepModel::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]; } struct sortInternalDegree { - StrongSolverTheoryUf::ConflictFind::Region* r; + StrongSolverTheoryUf::SortRepModel::Region* r; bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumInternalDisequalities()>r->d_nodes[j]->getNumInternalDisequalities());} }; struct sortExternalDegree { - StrongSolverTheoryUf::ConflictFind::Region* r; + StrongSolverTheoryUf::SortRepModel::Region* r; bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumExternalDisequalities()>r->d_nodes[j]->getNumExternalDisequalities());} }; -bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality ){ +int gmcCount = 0; + +bool StrongSolverTheoryUf::SortRepModel::Region::getMustCombine( int cardinality ){ if( options::ufssRegions() && 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 @@ -218,11 +214,10 @@ bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality } } } - //static int gmcCount = 0; - //gmcCount++; - //if( gmcCount%100==0 ){ - // std::cout << gmcCount << " " << cardinality << std::endl; - //} + gmcCount++; + if( gmcCount%100==0 ){ + Trace("gmc-count") << gmcCount << " " << cardinality << " sample : " << degrees.size() << std::endl; + } //this should happen relatively infrequently.... std::sort( degrees.begin(), degrees.end() ); for( int i=0; i<(int)degrees.size(); i++ ){ @@ -234,16 +229,21 @@ bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality return false; } -bool StrongSolverTheoryUf::ConflictFind::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){ +bool StrongSolverTheoryUf::SortRepModel::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){ if( d_reps_size>long(cardinality) ){ if( 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 ); + if( 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 ); + } } + Trace("quick-clique") << "Found quick clique" << std::endl; + return true; + }else{ + return false; } - return true; }else if( options::ufssRegions() || options::ufssEagerSplits() || level==Theory::EFFORT_FULL ){ //build test clique, up to size cardinality+1 if( d_testCliqueSize<=long(cardinality) ){ @@ -318,7 +318,7 @@ bool StrongSolverTheoryUf::ConflictFind::Region::check( Theory::Effort level, in return false; } -void StrongSolverTheoryUf::ConflictFind::Region::getRepresentatives( std::vector< Node >& reps ){ +void StrongSolverTheoryUf::SortRepModel::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 ){ @@ -327,7 +327,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::getRepresentatives( std::vector } } -void StrongSolverTheoryUf::ConflictFind::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){ +void StrongSolverTheoryUf::SortRepModel::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 ){ @@ -341,98 +341,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::getNumExternalDisequalities( st } } -Node StrongSolverTheoryUf::ConflictFind::Region::getBestSplit(){ -#ifndef USE_SMART_SPLITS - //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(); -#else - std::vector< Node > splits; - for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){ - if( (*it).second ){ - splits.push_back( (*it).first ); - } - } - if( splits.size()>1 ){ - std::map< Node, std::map< Node, bool > > ops; - Debug("uf-ss-split") << "Choice for splits: " << std::endl; - double maxScore = -1; - int maxIndex; - for( int i=0; i<(int)splits.size(); i++ ){ - Debug("uf-ss-split") << " " << splits[i] << std::endl; - for( int j=0; j<2; j++ ){ - if( ops.find( splits[i][j] )==ops.end() ){ - EqClassIterator eqc( splits[i][j], ((uf::TheoryUF*)d_cf->d_th)->getEqualityEngine() ); - while( !eqc.isFinished() ){ - Node n = (*eqc); - if( n.getKind()==APPLY_UF ){ - ops[ splits[i][j] ][ n.getOperator() ] = true; - } - ++eqc; - } - } - } - //now, compute score - int common[2] = { 0, 0 }; - for( int j=0; j<2; j++ ){ - int j2 = j==0 ? 1 : 0; - for( std::map< Node, bool >::iterator it = ops[ splits[i][j] ].begin(); it != ops[ splits[i][j] ].end(); ++it ){ - if( ops[ splits[i][j2] ].find( it->first )!=ops[ splits[i][j2] ].end() ){ - common[0]++; - }else{ - common[1]++; - } - } - } - double score = ( 1.0 + (double)common[0] )/( 1.0 + (double)common[1] ); - if( score>maxScore ){ - maxScore = score; - maxIndex = i; - } - } - //if( maxIndex!=0 ){ - // std::cout << "Chose maxIndex = " << maxIndex << std::endl; - //} - return splits[maxIndex]; - }else if( !splits.empty() ){ - return splits[0]; - }else{ - return Node::null(); - } -#endif -} - -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 ); -} - -bool StrongSolverTheoryUf::ConflictFind::Region::minimize( OutputChannel* out ){ - if( hasSplits() ){ - addSplit( out ); - return false; - }else{ - return true; - } -} - -void StrongSolverTheoryUf::ConflictFind::Region::debugPrint( const char* c, bool incClique ){ +void StrongSolverTheoryUf::SortRepModel::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; @@ -474,238 +383,431 @@ void StrongSolverTheoryUf::ConflictFind::Region::debugPrint( const char* c, bool } } -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++; + + + + + + + +StrongSolverTheoryUf::SortRepModel::SortRepModel( Node n, context::Context* c, TheoryUF* th ) : RepModel( n.getType() ), + d_th( th ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ), + d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( 0 ), + d_cardinality_assertions( c ), d_hasCard( c, false ){ + d_cardinality_term = n; +} + +/** initialize */ +void StrongSolverTheoryUf::SortRepModel::initialize( OutputChannel* out ){ + allocateCardinality( out ); +} + +/** new node */ +void StrongSolverTheoryUf::SortRepModel::newEqClass( Node n ){ + if( !d_conflict ){ + if( d_regions_map.find( n )==d_regions_map.end() ){ + if( !options::ufssTotalityLazy() ){ + //must generate totality axioms for every cardinality we have allocated thus far + for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){ + if( applyTotality( it->first ) ){ + addTotalityAxiom( n, it->first, &d_th->getOutputChannel() ); + } + } } + if( options::ufssTotality() ){ + //regions map will store whether we need to equate this term with a constant equivalence class + if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){ + d_regions_map[n] = 0; + }else{ + d_regions_map[n] = -1; + } + }else{ + if( !options::ufssRegions() ){ + //if not using regions, always add new equivalence classes to region index = 0 + d_regions_index = 0; + } + d_regions_map[n] = d_regions_index; + if( options::ufssSmartSplits() ){ + setSplitScore( n, 0 ); + } + 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( !options::ufssRegions() || d_regions[ d_regions_index ]->getNumReps()==0 ); + }else{ + d_regions.push_back( new Region( this, d_th->getSatContext() ) ); + } + d_regions[ d_regions_index ]->addRep( n ); + d_regions_index = d_regions_index + 1; + } + d_reps = d_reps + 1; } } - 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 ){ - 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 ] ]++; +/** merge */ +void StrongSolverTheoryUf::SortRepModel::merge( Node a, Node b ){ + if( !d_conflict ){ + if( options::ufssTotality() ){ + if( d_regions_map[b]==-1 ){ + d_regions_map[a] = -1; + } + d_regions_map[b] = -1; + }else{ + //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 ){ + int ri = combineRegions( bi, ai ); + d_regions[ri]->setEqual( a, b ); + checkRegion( ri ); + }else if( d_regions[bi]->getNumReps()==1 ){ + int ri = combineRegions( ai, bi ); + d_regions[ri]->setEqual( a, b ); + checkRegion( ri ); + }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_regions_map[b] = -1; } + d_reps = d_reps - 1; + Debug("uf-ss") << "Done merge." << std::endl; } } } -void StrongSolverTheoryUf::ConflictFind::explainClique( std::vector< Node >& clique, OutputChannel* out ){ - Assert( d_cardinality>0 ); - while( clique.size()>size_t(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()==(clique.size()*( clique.size()-1 )/2) ){ - break; +/** assert terms are disequal */ +void StrongSolverTheoryUf::SortRepModel::assertDisequal( Node a, Node b, Node reason ){ + if( !d_conflict ){ + if( options::ufssTotality() ){ + //do nothing + }else{ + //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; } } } - //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] ); +} + + +/** check */ +void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChannel* out ){ + if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){ + 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{ + if( applyTotality( d_cardinality ) ){ + //if we are applying totality to this cardinality + if( options::ufssTotalityLazy() ){ + //add totality axioms for all nodes that have not yet been equated to cardinality terms + if( level==Theory::EFFORT_FULL ){ + for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){ + if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){ + addTotalityAxiom( (*it).first, d_cardinality, &d_th->getOutputChannel() ); + } + } + } + } + }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 ) ){ + //add clique lemma + addCliqueLemma( clique, out ); + return; + }else{ + Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl; + } + } + } + bool addedLemma = false; + //do splitting on demand + if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){ + Trace("uf-ss-debug") << "Add splits?" << std::endl; + //see if we have any recommended splits from large regions + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid && d_regions[i]->getNumReps()>d_cardinality ){ + if( addSplit( d_regions[i], out ) ){ + addedLemma = true; +#ifdef ONE_SPLIT_REGION + break; +#endif + } + } + } + } + //if no added lemmas, force continuation via combination of regions + if( level==Theory::EFFORT_FULL ){ + if( !addedLemma ){ + Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl; + if( !options::ufssColoringSat() ){ + bool recheck = false; + //naive strategy, force region combination involving the first valid region + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + forceCombineRegion( i, false ); + recheck = true; + break; + } + } + if( recheck ){ + check( level, out ); + } } } } - 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 ); +} + +void StrongSolverTheoryUf::SortRepModel::propagate( Theory::Effort level, OutputChannel* out ){ - //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() ){ - if( !options::ufssRegions() ){ - //if not using regions, always add new equivalence classes to region index = 0 - d_regions_index = 0; - } - 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( !options::ufssRegions() || d_regions[ d_regions_index ]->getNumReps()==0 ); - }else{ - d_regions.push_back( new Region( this, d_th->getSatContext() ) ); +Node StrongSolverTheoryUf::SortRepModel::getNextDecisionRequest(){ + //request the current cardinality as a decision literal, if not already asserted + for( int i=1; i<=d_aloc_cardinality; i++ ){ + if( !d_hasCard || i<d_cardinality ){ + Node cn = d_cardinality_literal[ i ]; + Assert( !cn.isNull() ); + if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){ + Trace("uf-ss-dec") << "Propagate as decision " << d_type << " " << i << std::endl; + return cn; + } } - d_regions[ d_regions_index ]->addRep( n ); - d_regions_index = d_regions_index + 1; - d_reps = d_reps + 1; } + return Node::null(); } -/** 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 ){ - int ri = combineRegions( bi, ai ); - d_regions[ri]->setEqual( a, b ); - checkRegion( ri ); - }else if( d_regions[bi]->getNumReps()==1 ){ - int ri = combineRegions( ai, bi ); - d_regions[ri]->setEqual( a, b ); - checkRegion( ri ); - }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 ); +bool StrongSolverTheoryUf::SortRepModel::minimize( OutputChannel* out, TheoryModel* m ){ + if( options::ufssTotality() ){ + //do nothing + }else{ + if( m ){ +#if 0 + // ensure that the constructed model is minimal + // if the model has terms that the strong solver does not know about + if( (int)m->d_rep_set.d_type_reps[ d_type ].size()>d_cardinality ){ + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + if( eqc.getType()==d_type ){ + //we must ensure that this equivalence class has been accounted for + if( d_regions_map.find( eqc )==d_regions_map.end() ){ + //split on unaccounted for term and cardinality lemma term (as default) + Node splitEq = eqc.eqNode( d_cardinality_term ); + splitEq = Rewriter::rewrite( splitEq ); + Trace("uf-ss-minimize") << "Last chance minimize : " << splitEq << std::endl; + out->split( splitEq ); + //tell the sat solver to explore the equals branch first + out->requirePhase( splitEq, true ); + ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas ); + return false; + } + } + ++eqcs_i; } - checkRegion( ai ); - checkRegion( bi ); + Assert( false ); } +#endif }else{ - d_regions[ai]->setEqual( a, b ); - checkRegion( ai ); + //internal minimize, ensure that model forms a clique: + // if two equivalence classes are neither equal nor disequal, add a split + 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( addSplit( d_regions[validRegionIndex], out ) ){ + return false; + } + }else{ + validRegionIndex = i; + } + } + } + if( addSplit( d_regions[validRegionIndex], out ) ){ + return false; + } } - d_reps = d_reps - 1; - d_regions_map[b] = -1; } - Debug("uf-ss") << "Done merge." << std::endl; + return true; } -/** 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 ); + +int StrongSolverTheoryUf::SortRepModel::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++; + } } - 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 ); + } + return counter; +} + +void StrongSolverTheoryUf::SortRepModel::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 ){ + 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 ] ]++; + } + } } - //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; +void StrongSolverTheoryUf::SortRepModel::setSplitScore( Node n, int s ){ + if( d_split_score.find( n )!=d_split_score.end() ){ + int ss = d_split_score[ n ]; + d_split_score[ n ] = s>ss ? s : ss; + }else{ + d_split_score[ n ] = s; + } + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + setSplitScore( n[i], s+1 ); + } +} + +void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out, int c, bool val ){ + if( !d_conflict ){ + Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = " << d_th->d_valuation.getAssertionLevel() << std::endl; + Assert( d_cardinality_literal.find( c )!=d_cardinality_literal.end() ); + d_cardinality_assertions[ d_cardinality_literal[c] ] = val; + if( val ){ + bool doCheckRegions = !d_hasCard; + if( !d_hasCard || c<d_cardinality ){ + d_cardinality = c; + } + d_hasCard = true; + //should check all regions now + if( doCheckRegions ){ + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + checkRegion( i ); + if( d_conflict ){ + return; + } + } + } + } + }else{ + if( options::ufssModelInference() ){ + //check if we are at decision level 0 + if( d_th->d_valuation.getAssertionLevel()==0 ){ + Trace("uf-ss-mi") << "We have proved that no models of size " << c << " for type " << d_type << " exist." << std::endl; + Trace("uf-ss-mi") << " # Clique lemmas : " << d_cliques[c].size() << std::endl; + if( d_cliques[c].size()==1 ){ + if( d_totality_terms[c+1].empty() ){ + Trace("uf-ss-mi") << "*** Establish model" << std::endl; + //d_totality_terms[c+1].insert( d_totality_terms[c].begin(), d_cliques[c][0].begin(), d_cliques[c][0].end() ); + } + } + } + } + //see if we need to request a new cardinality + if( !d_hasCard ){ + bool needsCard = true; + for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){ + if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){ + needsCard = false; + break; + } + } + if( needsCard ){ + allocateCardinality( out ); + } + } + } } } -void StrongSolverTheoryUf::ConflictFind::checkRegion( int ri, bool rec ){ - if( isValid(ri) ){ +void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool rec ){ + if( isValid(ri) && d_hasCard ){ 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() ); + addCliqueLemma( clique, &d_th->getOutputChannel() ); }else if( d_regions[ri]->getMustCombine( d_cardinality ) ){ ////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 ){ @@ -724,7 +826,7 @@ void StrongSolverTheoryUf::ConflictFind::checkRegion( int ri, bool rec ){ } } -int StrongSolverTheoryUf::ConflictFind::forceCombineRegion( int ri, bool useDensity ){ +int StrongSolverTheoryUf::SortRepModel::forceCombineRegion( int ri, bool useDensity ){ if( !useDensity ){ for( int i=0; i<(int)d_regions_index; i++ ){ if( ri!=i && d_regions[i]->d_valid ){ @@ -764,7 +866,7 @@ int StrongSolverTheoryUf::ConflictFind::forceCombineRegion( int ri, bool useDens } -int StrongSolverTheoryUf::ConflictFind::combineRegions( int ai, int bi ){ +int StrongSolverTheoryUf::SortRepModel::combineRegions( int ai, int bi ){ #ifdef COMBINE_REGIONS_SMALL_INTO_LARGE if( d_regions[ai]->getNumReps()<d_regions[bi]->getNumReps() ){ return combineRegions( bi, ai ); @@ -784,7 +886,7 @@ int StrongSolverTheoryUf::ConflictFind::combineRegions( int ai, int bi ){ return ai; } -void StrongSolverTheoryUf::ConflictFind::moveNode( Node n, int ri ){ +void StrongSolverTheoryUf::SortRepModel::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 ) ); @@ -793,161 +895,248 @@ void StrongSolverTheoryUf::ConflictFind::moveNode( Node n, int ri ){ d_regions_map[n] = ri; } -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 - quantifiers::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" ) << "*** Disambiguate lemma : " << lem << std::endl; - //Notice() << "*** Disambiguate lemma : " << lem << std::endl; - out->lemma( lem ); - d_term_amb[ eq ] = false; - lemmaAdded = true; - ++( d_th->getStrongSolver()->d_statistics.d_disamb_term_lemmas ); - } - } - } +void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out ){ + if( d_aloc_cardinality>0 ){ + Trace("uf-ss-fmf") << "No model of size " << d_aloc_cardinality << " exists for type " << d_type << " in this branch" << std::endl; + if( Trace.isOn("uf-ss-cliques") ){ + Trace("uf-ss-cliques") << "Cliques of size " << (d_aloc_cardinality+1) << " : " << std::endl; + for( size_t i=0; i<d_cliques[ d_aloc_cardinality ].size(); i++ ){ + Trace("uf-ss-cliques") << " "; + for( size_t j=0; j<d_cliques[ d_aloc_cardinality ][i].size(); j++ ){ + Trace("uf-ss-cliques") << d_cliques[ d_aloc_cardinality ][i][j] << " "; } + Trace("uf-ss-cliques") << std::endl; + } + } + } + d_aloc_cardinality++; + + //check for abort case + if( options::ufssAbortCardinality()==d_aloc_cardinality ){ + //abort here DO_THIS + Message() << "Maximum cardinality reached." << std::endl; + exit( 0 ); + }else{ + if( options::ufssTotality() ){ + //must generate new cardinality lemma term + std::stringstream ss; + ss << "_c_" << d_aloc_cardinality; + Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type ); + d_totality_terms[0].push_back( var ); + Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl; + //must be distinct from all other cardinality terms + for( int i=0; i<(int)(d_totality_terms[0].size()-1); i++ ){ + Node lem = NodeManager::currentNM()->mkNode( NOT, var.eqNode( d_totality_terms[0][i] ) ); + d_th->getOutputChannel().lemma( lem ); + } + } + + //add splitting lemma for cardinality constraint + Assert( !d_cardinality_term.isNull() ); + Node lem = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_term, + NodeManager::currentNM()->mkConst( Rational( d_aloc_cardinality ) ) ); + lem = Rewriter::rewrite(lem); + d_cardinality_literal[ d_aloc_cardinality ] = lem; + lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); + d_cardinality_lemma[ d_aloc_cardinality ] = lem; + //add as lemma to output channel + out->lemma( lem ); + //require phase + out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true ); + //add the appropriate lemma, propagate as decision + //Trace("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << " " << d_type << std::endl; + //out->propagateAsDecision( lem[0] ); + d_th->getStrongSolver()->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality ); + + if( applyTotality( d_aloc_cardinality ) && !options::ufssTotalityLazy() ){ + //must send totality axioms for each existing term + for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){ + addTotalityAxiom( (*it).first, d_aloc_cardinality, &d_th->getOutputChannel() ); } } } - 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 << " "; +bool StrongSolverTheoryUf::SortRepModel::addSplit( Region* r, OutputChannel* out ){ + if( r->hasSplits() ){ + Node s; + if( !options::ufssSmartSplits() ){ + //take the first split you find + for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){ + if( (*it).second ){ + s = (*it).first; + break; + } } - 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; + int maxScore = -1; + std::vector< Node > splits; + for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){ + if( (*it).second ){ + int score1 = d_split_score[ (*it).first[0] ]; + int score2 = d_split_score[ (*it).first[1] ]; + int score = score1<score2 ? score1 : score2; + if( score>maxScore ){ + maxScore = -1; + s = (*it).first; } } } - bool addedLemma = false; - //do splitting on demand - if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){ - Debug("uf-ss-debug") << "Add splits?" << std::endl; - //see if we have any recommended splits from large regions - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid && d_regions[i]->getNumReps()>d_cardinality ){ - if( d_regions[i]->hasSplits() ){ - d_regions[i]->addSplit( out ); - addedLemma = true; - ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas ); -#ifdef ONE_SPLIT_REGION - break; -#endif - } - } - } + } + //add lemma to output channel + Assert( s!=Node::null() && s.getKind()==EQUAL ); + s = Rewriter::rewrite( s ); + Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; + //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " "; + //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl; + //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; + //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 ); + ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas ); + return true; + }else{ + return false; + } +} + + +void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){ + Assert( d_hasCard ); + Assert( d_cardinality>0 ); + while( clique.size()>size_t(d_cardinality+1) ){ + clique.pop_back(); + } + if( options::ufssModelInference() || Trace.isOn("uf-ss-cliques") ){ + std::vector< Node > clique_vec; + clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); + d_cliques[ d_cardinality ].push_back( clique_vec ); + } + + //found a clique + Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl; + Debug("uf-ss-cliques") << " "; + for( int i=0; i<(int)clique.size(); i++ ){ + Debug("uf-ss-cliques") << clique[i] << " "; + } + Debug("uf-ss-cliques") << std::endl; + Debug("uf-ss-cliques") << "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] ); + Debug("uf-ss-cliques") << " -> disequality : " << d_disequalities[i] << std::endl; + nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true; + nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true; + if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){ + break; } - //force continuation via term disambiguation or combination of regions - if( level==Theory::EFFORT_FULL ){ - if( !addedLemma ){ - Debug("uf-ss") << "No splits added." << std::endl; - if( options::ufssColoringSat() ){ - //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{ - bool recheck = false; - //naive strategy, force region combination involving the first valid region - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ - forceCombineRegion( i, false ); - recheck = true; - break; - } - } - if( recheck ){ - check( level, out ); + } + } + //Debug("uf-ss-cliques") << 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-cliques") << "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 + Debug("uf-ss-cliques") << "Explain "; + for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + if( prev!=Node::null() ){ + Debug("uf-ss-cliques") << " = "; + //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-cliques") << prev; } + Debug("uf-ss-cliques") << std::endl; } } + Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl; + for( int i=0; i<(int)conflict.size(); i++ ){ + Debug("uf-ss-cliques") << conflict[i] << " "; + //bool value; + //bool hasValue = d_th->getValuation().hasSatValue( conflict[i], value ); + //Assert( hasValue ); + //Assert( value ); + } + Debug("uf-ss-cliques") << std::endl; + //now, make the conflict +#if 1 + conflict.push_back( d_cardinality_literal[ d_cardinality ] ); + Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict ); + Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl; + //Notice() << "*** Add clique conflict " << conflictNode << std::endl; + out->conflict( conflictNode ); + d_conflict = true; +#else + Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict ); + //add cardinality constraint + Node cardNode = d_cardinality_literal[ d_cardinality ]; + //bool value; + //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value ); + //Assert( hasValue ); + //Assert( value ); + conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() ); + Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl; + //Notice() << "*** Add clique conflict " << conflictNode << std::endl; + out->lemma( conflictNode ); +#endif + ++( 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. } -void StrongSolverTheoryUf::ConflictFind::propagate( Theory::Effort level, OutputChannel* out ){ - Assert( d_cardinality>0 ); - //propagate the current cardinality as a decision literal, if not already asserted - 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::SortRepModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){ + Node cardLit = d_cardinality_literal[ cardinality ]; + std::vector< Node > eqs; + for( int i=0; i<cardinality; i++ ){ + eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) ); } + Node ax = NodeManager::currentNM()->mkNode( OR, eqs ); + Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax ); + Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl; + //send as lemma to the output channel + d_th->getOutputChannel().lemma( lem ); + ++( d_th->getStrongSolver()->d_statistics.d_totality_lemmas ); } -void StrongSolverTheoryUf::ConflictFind::debugPrint( const char* c ){ +/** apply totality */ +bool StrongSolverTheoryUf::SortRepModel::applyTotality( int cardinality ){ + return options::ufssTotality() || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() ); +} + +/** get totality lemma terms */ +Node StrongSolverTheoryUf::SortRepModel::getTotalityLemmaTerm( int cardinality, int i ){ + if( options::ufssTotality() ){ + return d_totality_terms[0][i]; + }else{ + return d_totality_terms[cardinality][i]; + } +} + +void StrongSolverTheoryUf::SortRepModel::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; @@ -972,7 +1161,32 @@ void StrongSolverTheoryUf::ConflictFind::debugPrint( const char* c ){ } } -int StrongSolverTheoryUf::ConflictFind::getNumRegions(){ +void StrongSolverTheoryUf::SortRepModel::debugModel( TheoryModel* m ){ + std::vector< Node > eqcs; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + if( eqc.getType()==d_type ){ + if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){ + eqcs.push_back( eqc ); + //we must ensure that this equivalence class has been accounted for + if( d_regions_map.find( eqc )==d_regions_map.end() ){ + Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl; + Trace("uf-ss-warn") << " type : " << d_type << std::endl; + Trace("uf-ss-warn") << " kind : " << eqc.getKind() << std::endl; + } + } + } + ++eqcs_i; + } + if( (int)eqcs.size()!=d_cardinality ){ + Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl; + Trace("uf-ss-warn") << " cardinality : " << d_cardinality << std::endl; + Trace("uf-ss-warn") << " # reps : " << (int)eqcs.size() << std::endl; + } +} + +int StrongSolverTheoryUf::SortRepModel::getNumRegions(){ int count = 0; for( int i=0; i<(int)d_regions_index; i++ ){ if( d_regions[i]->d_valid ){ @@ -982,25 +1196,7 @@ int StrongSolverTheoryUf::ConflictFind::getNumRegions(){ 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 ){ +void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node >& reps ){ if( !options::ufssColoringSat() ){ bool foundRegion = false; for( int i=0; i<(int)d_regions_index; i++ ){ @@ -1019,87 +1215,158 @@ void StrongSolverTheoryUf::ConflictFind::getRepresentatives( std::vector< Node > } } -bool StrongSolverTheoryUf::ConflictFind::minimize( OutputChannel* out ){ - //ensure that model forms a clique: - // if two equivalence classes are neither equal nor disequal, add a split - 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; + +/** initialize */ +void StrongSolverTheoryUf::InfRepModel::initialize( OutputChannel* out ){ + +} + +/** new node */ +void StrongSolverTheoryUf::InfRepModel::newEqClass( Node n ){ + d_rep[n] = n; + //d_const_rep[n] = n.getMetaKind()==metakind::CONSTANT; +} + +/** merge */ +void StrongSolverTheoryUf::InfRepModel::merge( Node a, Node b ){ + //d_rep[b] = false; + //d_const_rep[a] = d_const_rep[a] || d_const_rep[b]; + Node repb = d_rep[b]; + Assert( !repb.isNull() ); + if( repb.getMetaKind()==metakind::CONSTANT || isBadRepresentative( d_rep[a] ) ){ + d_rep[a] = repb; + } + d_rep[b] = Node::null(); +} + +/** check */ +void StrongSolverTheoryUf::InfRepModel::check( Theory::Effort level, OutputChannel* out ){ + +} + +/** minimize */ +bool StrongSolverTheoryUf::InfRepModel::minimize( OutputChannel* out ){ +#if 0 + bool retVal = true; +#else + bool retVal = !addSplit( out ); +#endif + if( retVal ){ + std::vector< Node > reps; + getRepresentatives( reps ); + Trace("uf-ss-fmf") << "Num representatives of type " << d_type << " : " << reps.size() << std::endl; + /* + for( int i=0; i<(int)reps.size(); i++ ){ + std::cout << reps[i] << " "; + } + std::cout << std::endl; + for( int i=0; i<(int)reps.size(); i++ ){ + std::cout << reps[i].getMetaKind() << " "; + } + std::cout << std::endl; + for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){ + Node rep = (*it).second; + if( !rep.isNull() && !isBadRepresentative( rep ) ){ + for( NodeNodeMap::iterator it2 = d_rep.begin(); it2 != d_rep.end(); ++it2 ){ + Node rep2 = (*it2).second; + if( !rep2.isNull() && !isBadRepresentative( rep2 ) ){ + if( d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, rep2 ) ){ + std::cout << "1 "; + }else{ + std::cout << "0 "; + } + } } - }else{ - validRegionIndex = i; + //std::cout << " : " << rep; + std::cout << std::endl; } } + */ } - if( !d_regions[validRegionIndex]->minimize( out ) ){ - return false; + return retVal; +} + +/** get representatives */ +void StrongSolverTheoryUf::InfRepModel::getRepresentatives( std::vector< Node >& reps ){ + for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){ + if( !(*it).second.isNull() ){ + reps.push_back( (*it).first ); + } } - 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 << Expr::setlanguage(options::outputLanguage()); - ss << "t_" << d_type; - d_cardinality_lemma_term = NodeManager::currentNM()->mkSkolem( ss.str(), d_type ); +/** add split function */ +bool StrongSolverTheoryUf::InfRepModel::addSplit( OutputChannel* out ){ + std::vector< Node > visited; + for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){ + Node rep = (*it).second; + if( !rep.isNull() && !isBadRepresentative( rep ) ){ + bool constRep = rep.getMetaKind()==metakind::CONSTANT; + for( size_t i=0; i<visited.size(); i++ ){ + if( !constRep || !visited[i].getMetaKind()==metakind::CONSTANT ){ + if( !d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, visited[i] ) ){ + //split on these nodes + Node eq = rep.eqNode( visited[i] ); + Trace("uf-ss-lemma") << "*** Split on " << eq << std::endl; + eq = Rewriter::rewrite( eq ); + Debug("uf-ss-lemma-debug") << "Rewritten " << eq << std::endl; + out->split( eq ); + //explore the equals branch first + out->requirePhase( eq, true ); + ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas ); + return true; + } + } + } + visited.push_back( rep ); } - 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 ]; + return false; +} + +bool StrongSolverTheoryUf::InfRepModel::isBadRepresentative( Node n ){ + return n.getKind()==kind::PLUS; } StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : d_out( &out ), d_th( th ), -d_conf_find(), +d_conflict( c, false ), +d_rep_model(), d_conf_types(), -d_conf_find_init( c ) +d_rep_model_init( c ) { - + if( options::ufssColoringSat() ){ + d_term_amb = new TermDisambiguator( th->getQuantifiersEngine(), c ); + }else{ + d_term_amb = NULL; + } } /** new node */ void StrongSolverTheoryUf::newEqClass( Node n ){ - TypeNode tn = n.getType(); - ConflictFind* c = getConflictFind( tn ); + RepModel* c = getRepModel( n ); if( c ){ - Debug("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl; + Trace("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " : " << n.getType() << std::endl; c->newEqClass( n ); } - //else if( tn.isSort() ){ - // //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 ); + RepModel* c = getRepModel( a ); if( c ){ - Debug("uf-ss-solver") << "StrongSolverTheoryUf: Merge " << a << " " << b << " " << tn << std::endl; + Trace("uf-ss-solver") << "StrongSolverTheoryUf: Merge " << a << " " << b << " : " << a.getType() << std::endl; c->merge( a, b ); } } /** assert terms are disequal */ void StrongSolverTheoryUf::assertDisequal( Node a, Node b, Node reason ){ - TypeNode tn = a.getType(); - ConflictFind* c = getConflictFind( tn ); + RepModel* c = getRepModel( a ); if( c ){ - Debug("uf-ss-solver") << "StrongSolverTheoryUf: Assert disequal " << a << " " << b << " " << tn << std::endl; + Trace("uf-ss-solver") << "StrongSolverTheoryUf: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl; //Assert( d_th->d_equalityEngine.getRepresentative( a )==a ); //Assert( d_th->d_equalityEngine.getRepresentative( b )==b ); c->assertDisequal( a, b, reason ); @@ -1108,88 +1375,89 @@ void StrongSolverTheoryUf::assertDisequal( Node a, Node b, Node reason ){ /** assert a node */ void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){ - Debug("uf-ss-assert") << "Assert " << n << " " << isDecision << std::endl; + Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl; if( n.getKind()==CARDINALITY_CONSTRAINT ){ TypeNode tn = n[0].getType(); - Assert( d_conf_find[tn]->getCardinality()>0 ); Assert( tn.isSort() ); - Assert( d_conf_find[tn] ); + Assert( d_rep_model[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; - } + d_rep_model[tn]->assertCardinality( d_out, nCard, true ); }else if( n.getKind()==NOT && n[0].getKind()==CARDINALITY_CONSTRAINT ){ - //must add new lemma Node nn = n[0]; TypeNode tn = nn[0].getType(); Assert( tn.isSort() ); - Assert( d_conf_find[tn] ); + Assert( d_rep_model[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 ); - } + d_rep_model[tn]->assertCardinality( d_out, nCard, false ); }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(); - // } - // } - //} + if( isDecision ){ + for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + if( !it->second->hasCardinalityAsserted() ){ + Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl; + //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl; + //Unimplemented(); + } + } + } } + Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl; } /** 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 ); + if( !d_conflict ){ + Trace("uf-ss-solver") << "StrongSolverTheoryUf: check " << level << std::endl; + if( level==Theory::EFFORT_FULL ){ + debugPrint( "uf-ss-debug" ); + } + for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + it->second->check( level, d_out ); + if( it->second->isConflict() ){ + d_conflict = true; + break; + } + } + //disambiguate terms if necessary + if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){ + Assert( d_term_amb!=NULL ); + d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out ); + } + Trace("uf-ss-solver") << "Done StrongSolverTheoryUf: check " << level << std::endl; } - 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 ); - } + //for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.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( tn.isSort() ){ - preRegisterType( tn ); +/** get next decision request */ +Node StrongSolverTheoryUf::getNextDecisionRequest(){ + for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + Node n = it->second->getNextDecisionRequest(); + if( !n.isNull() ){ + return n; + } } + return Node::null(); } -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(); +void StrongSolverTheoryUf::preRegisterTerm( TNode n ){ + //shouldn't have to preregister this type (it may be that there are no quantifiers over tn) + TypeNode tn = n.getType(); + if( d_rep_model.find( tn )==d_rep_model.end() ){ + RepModel* rm = NULL; if( tn.isSort() ){ - preRegisterType( tn ); + Debug("uf-ss-register") << "Preregister sort " << tn << "." << std::endl; + rm = new SortRepModel( n, d_th->getSatContext(), d_th ); + }else if( tn.isInteger() ){ + //rm = new InfRepModel( tn, d_th->getSatContext(), d_th ); + //rm = new SortRepModel( tn, d_th->getSatContext(), d_th ); }else{ /* if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ @@ -1205,63 +1473,51 @@ void StrongSolverTheoryUf::registerQuantifier( Node f ){ } */ } + if( rm ){ + rm->initialize( d_out ); + d_rep_model[tn] = rm; + d_rep_model_init[tn] = true; + } } } -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 ); - } +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(); + // preRegisterType( tn, true ); + //} } -StrongSolverTheoryUf::ConflictFind* StrongSolverTheoryUf::getConflictFind( TypeNode tn ){ - std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.find( tn ); + +StrongSolverTheoryUf::RepModel* StrongSolverTheoryUf::getRepModel( Node n ){ + TypeNode tn = n.getType(); + std::map< TypeNode, RepModel* >::iterator it = d_rep_model.find( tn ); //pre-register the type if not done already - if( it==d_conf_find.end() ){ - if( tn.isSort() ){ - preRegisterType( tn ); - it = d_conf_find.find( tn ); - } + if( it==d_rep_model.end() ){ + preRegisterTerm( n ); + it = d_rep_model.find( tn ); } - if( it!=d_conf_find.end() ){ + if( it!=d_rep_model.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; - } + //if( d_rep_model_init.find( tn )==d_rep_model_init.end() ){ + ////initialize the model + //it->second->initialize( d_out ); + //d_rep_model_init[tn] = true; + //} return it->second; - }else{ - return NULL; } + 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 ); +int StrongSolverTheoryUf::getCardinality( Node n ) { + RepModel* c = getRepModel( n ); if( c ){ return c->getCardinality(); }else{ @@ -1269,28 +1525,22 @@ int StrongSolverTheoryUf::getCardinality( TypeNode t ) { } } -void StrongSolverTheoryUf::getRepresentatives( TypeNode t, std::vector< Node >& reps ){ - ConflictFind* c = getConflictFind( t ); +void StrongSolverTheoryUf::getRepresentatives( Node n, std::vector< Node >& reps ){ + RepModel* c = getRepModel( n ); 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 ) ){ +bool StrongSolverTheoryUf::minimize( TheoryModel* m ){ + for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + if( !it->second->minimize( d_out, m ) ){ return false; } } + for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + Trace("uf-ss-minimize") << "Cardinality( " << it->first << " ) : " << it->second->getCardinality() << std::endl; + } return true; } @@ -1309,22 +1559,32 @@ void StrongSolverTheoryUf::debugPrint( const char* c ){ // eqc_iter++; //} - for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){ + for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl; it->second->debugPrint( c ); Debug( c ) << std::endl; } } +void StrongSolverTheoryUf::debugModel( TheoryModel* m ){ + if( Trace.isOn("uf-ss-warn") ){ + for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + it->second->debugModel( m ); + } + } +} + 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) + d_totality_lemmas("StrongSolverTheoryUf::Totality_Lemmas", 0), + d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 1) { StatisticsRegistry::registerStat(&d_clique_lemmas); StatisticsRegistry::registerStat(&d_split_lemmas); StatisticsRegistry::registerStat(&d_disamb_term_lemmas); + StatisticsRegistry::registerStat(&d_totality_lemmas); StatisticsRegistry::registerStat(&d_max_model_size); } @@ -1332,10 +1592,70 @@ StrongSolverTheoryUf::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_clique_lemmas); StatisticsRegistry::unregisterStat(&d_split_lemmas); StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas); + StatisticsRegistry::unregisterStat(&d_totality_lemmas); StatisticsRegistry::unregisterStat(&d_max_model_size); } -bool StrongSolverTheoryUf::involvesRelevantType( Node n ){ + +int TermDisambiguator::disambiguateTerms( OutputChannel* out ){ + Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl; + int lemmaAdded = 0; + //otherwise, determine ambiguous pairs of ground terms for relevant sorts + quantifiers::TermDb* db = d_qe->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(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_qe->getEqualityQuery()->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_qe->getEqualityQuery()->areDisequal( it->second[i][k], it->second[j][k] ) ){ + 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" ) << "*** Disambiguate lemma : " << lem << std::endl; + //Notice() << "*** Disambiguate lemma : " << lem << std::endl; + out->lemma( lem ); + d_term_amb[ eq ] = false; + lemmaAdded++; + } + } + } + } + } + } + } + Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl; + return lemmaAdded; +} + +bool TermDisambiguator::involvesRelevantType( Node n ){ if( n.getKind()==APPLY_UF ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ if( n[i].getType().isSort() ){ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 479fea05f..8c63b4308 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -32,24 +32,63 @@ namespace theory { namespace uf { class TheoryUF; +class TermDisambiguator; class StrongSolverTheoryUf{ protected: typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; typedef context::CDChunkList<Node> NodeList; typedef context::CDList<bool> BoolList; typedef context::CDList<bool> IntList; typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap; public: + class RepModel { + protected: + /** type */ + TypeNode d_type; + public: + RepModel( TypeNode tn ) : d_type( tn ){} + virtual ~RepModel(){} + /** initialize */ + virtual void initialize( OutputChannel* out ) = 0; + /** new node */ + virtual void newEqClass( Node n ) = 0; + /** merge */ + virtual void merge( Node a, Node b ) = 0; + /** assert terms are disequal */ + virtual void assertDisequal( Node a, Node b, Node reason ) = 0; + /** check */ + virtual void check( Theory::Effort level, OutputChannel* out ){} + /** get next decision request */ + virtual Node getNextDecisionRequest() { return Node::null(); } + /** minimize */ + virtual bool minimize( OutputChannel* out, TheoryModel* m ){ return true; } + /** assert cardinality */ + virtual void assertCardinality( OutputChannel* out, int c, bool val ){} + /** is in conflict */ + virtual bool isConflict() { return false; } + /** get cardinality */ + virtual int getCardinality() { return -1; } + /** has cardinality */ + virtual bool hasCardinalityAsserted() { return true; } + /** get representatives */ + virtual void getRepresentatives( std::vector< Node >& reps ){} + /** print debug */ + virtual void debugPrint( const char* c ){} + /** debug a model */ + virtual void debugModel( TheoryModel* m ){} + }; +public: /** information for incremental conflict/clique finding for a particular sort */ - class ConflictFind { + class SortRepModel : public RepModel { public: /** a partition of the current equality graph for which cliques can occur internally */ class Region { public: /** conflict find pointer */ - ConflictFind* d_cf; + SortRepModel* d_cf; /** information stored about each node in region */ class RegionNodeInfo { public: @@ -86,14 +125,13 @@ public: }; ///** end class RegionNodeInfo */ private: + context::CDO< unsigned > d_testCliqueSize; + context::CDO< unsigned > d_splitsSize; + public: //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; @@ -106,11 +144,11 @@ public: void setRep( Node n, bool valid ); 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( SortRepModel* cf, context::Context* c ) : d_cf( cf ), d_testCliqueSize( c, 0 ), + d_splitsSize( c, 0 ), d_testClique( c ), d_splits( c ), d_reps_size( c, 0 ), + d_total_diseq_external( c, 0 ), d_total_diseq_internal( c, 0 ), d_valid( c, true ) { } - ~Region(){} + virtual ~Region(){} //region node infomation std::map< Node, RegionNodeInfo* > d_nodes; //whether region is valid @@ -146,10 +184,6 @@ public: public: /** check for cliques */ bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique ); - /** add split */ - void addSplit( OutputChannel* out ); - /** minimize */ - bool minimize( OutputChannel* out ); //print debug void debugPrint( const char* c, bool incClique = false ); }; @@ -162,25 +196,23 @@ public: std::vector< Region* > d_regions; /** map from Nodes to index of d_regions they exist in, -1 means invalid */ NodeIntMap d_regions_map; + /** the score for each node for splitting */ + NodeIntMap d_split_score; /** 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: /** 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 ); - /** 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 ); + /** set split score */ + void setSplitScore( Node n, int s ); private: /** check if we need to combine region ri */ void checkRegion( int ri, bool rec = true ); @@ -191,78 +223,131 @@ public: /** move node n to region ri */ void moveNode( Node n, int ri ); private: - /** cardinality operating with */ + /** allocate cardinality */ + void allocateCardinality( OutputChannel* out ); + /** add split */ + bool addSplit( Region* r, OutputChannel* out ); + /** add clique lemma */ + void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ); + /** add totality axiom */ + void addTotalityAxiom( Node n, int cardinality, OutputChannel* out ); + private: + /** Are we in conflict */ + context::CDO<bool> d_conflict; + /** cardinality */ context::CDO< int > d_cardinality; - /** type */ - TypeNode d_type; + /** maximum allocated cardinality */ + int d_aloc_cardinality; /** cardinality lemma term */ - Node d_cardinality_lemma_term; + Node d_cardinality_term; + /** cardinality totality terms */ + std::map< int, std::vector< Node > > d_totality_terms; /** 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; + /** whether a positive cardinality constraint has been asserted */ + context::CDO< bool > d_hasCard; + /** clique lemmas that have been asserted */ + std::map< int, std::vector< std::vector< Node > > > d_cliques; + private: + /** apply totality */ + bool applyTotality( int cardinality ); + /** get totality lemma terms */ + Node getTotalityLemmaTerm( int cardinality, int i ); 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(){} + SortRepModel( Node n, context::Context* c, TheoryUF* th ); + virtual ~SortRepModel(){} + /** initialize */ + void initialize( OutputChannel* out ); /** 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 next decision request */ + Node getNextDecisionRequest(); + /** minimize */ + bool minimize( OutputChannel* out, TheoryModel* m ); + /** assert cardinality */ + void assertCardinality( OutputChannel* out, int c, bool val ); + /** is in conflict */ + bool isConflict() { return d_conflict; } /** 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(); + /** has cardinality */ + bool hasCardinalityAsserted() { return d_hasCard; } + //print debug + void debugPrint( const char* c ); + /** debug a model */ + void debugModel( TheoryModel* m ); 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 */ + }; /** class SortRepModel */ +private: + /** infinite rep model */ + class InfRepModel : public RepModel + { + protected: + /** theory uf pointer */ + TheoryUF* d_th; + /** list of representatives */ + NodeNodeMap d_rep; + /** whether representatives are constant */ + NodeBoolMap d_const_rep; + /** add split */ + bool addSplit( OutputChannel* out ); + /** is bad representative */ + bool isBadRepresentative( Node n ); + public: + InfRepModel( TypeNode tn, context::Context* c, TheoryUF* th ) : RepModel( tn ), + d_th( th ), d_rep( c ), d_const_rep( c ){} + virtual ~InfRepModel(){} + /** initialize */ + void initialize( OutputChannel* out ); + /** 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 ){} + /** check */ + void check( Theory::Effort level, OutputChannel* out ); + /** minimize */ + bool minimize( OutputChannel* out ); + /** get representatives */ + void getRepresentatives( std::vector< Node >& reps ); + /** print debug */ + void debugPrint( const char* c ){} + }; 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; + /** Are we in conflict */ + context::CDO<bool> d_conflict; + /** rep model structure, one for each type */ + std::map< TypeNode, RepModel* > d_rep_model; /** 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 ); + TypeNodeBoolMap d_rep_model_init; /** get conflict find */ - ConflictFind* getConflictFind( TypeNode tn ); + RepModel* getRepModel( Node n ); +private: + /** term disambiguator */ + TermDisambiguator* d_term_amb; public: StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th); ~StrongSolverTheoryUf() {} @@ -279,6 +364,8 @@ public: void check( Theory::Effort level ); /** propagate */ void propagate( Theory::Effort level ); + /** get next decision request */ + Node getNextDecisionRequest(); /** preregister a term */ void preRegisterTerm( TNode n ); /** preregister a quantifier */ @@ -290,35 +377,52 @@ public: std::string identify() const { return std::string("StrongSolverTheoryUf"); } //print debug void debugPrint( const char* c ); + /** debug a model */ + void debugModel( TheoryModel* m ); 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 is in conflict */ + bool isConflict() { return d_conflict; } /** get cardinality for sort */ - int getCardinality( TypeNode t ); + int getCardinality( Node n ); /** get representatives */ - void getRepresentatives( TypeNode t, std::vector< Node >& reps ); - /** get cardinality term */ - //Node getCardinalityTerm( TypeNode t ); + void getRepresentatives( Node n, std::vector< Node >& reps ); /** minimize */ - bool minimize(); + bool minimize( TheoryModel* m = NULL ); class Statistics { public: IntStat d_clique_lemmas; IntStat d_split_lemmas; IntStat d_disamb_term_lemmas; + IntStat d_totality_lemmas; IntStat d_max_model_size; Statistics(); ~Statistics(); }; /** statistics class */ Statistics d_statistics; +};/* class StrongSolverTheoryUf */ + +class TermDisambiguator +{ +private: + /** quantifiers engine */ + QuantifiersEngine* d_qe; + /** whether two terms are ambiguous (indexed by equalities) */ + context::CDHashMap<Node, bool, NodeHashFunction> d_term_amb; /** involves relevant type */ static bool involvesRelevantType( Node n ); -};/* class StrongSolverTheoryUf */ +public: + TermDisambiguator( QuantifiersEngine* qe, context::Context* c ) : d_qe( qe ), d_term_amb( c ){} + ~TermDisambiguator(){} + /** check ambiguous terms */ + int disambiguateTerms( OutputChannel* out ); +}; } }/* CVC4::theory namespace */ diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index d00b69398..09f287884 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -72,68 +72,6 @@ public: } };/* class CardinalityConstraintTypeRule */ -class FunctionModelTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { - TypeNode tn = n[0].getType(check); - if( check ){ - if( n.getNumChildren()==2 ){ - if( n[0].getKind()!=kind::FUNCTION_CASE_SPLIT ){ - throw TypeCheckingExceptionPrivate(n, "improper function model representation : first child must be case split"); - } - TypeNode tn2 = n[1].getType(check); - if( tn!=tn2 ){ - std::stringstream ss; - ss << "function model has inconsistent return types : " << tn << " " << tn2; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - } - return tn; - } -};/* class FunctionModelTypeRule */ - -class FunctionCaseSplitTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { - TypeNode retType = n[0][1].getType(check); - if( check ){ - TypeNode argType = n[0][0].getType(check); - for( size_t i=0; i<n.getNumChildren(); i++ ){ - TypeNode argType2 = n[i][0].getType(check); - if( argType!=argType2 ){ - std::stringstream ss; - ss << "function case split has inconsistent argument types : " << argType << " " << argType2; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - TypeNode retType2 = n[i][1].getType(check); - if( retType!=retType2 ){ - std::stringstream ss; - ss << "function case split has inconsistent return types : " << retType << " " << retType2; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - } - return retType; - } -};/* class FunctionCaseSplitTypeRule */ - - -class FunctionCaseTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { - TypeNode retType = n[1].getType(check); - if( check ){ - TypeNode argType = n[0].getType(check); - } - return retType; - } -};/* class FunctionCaseTypeRule */ - - }/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |