diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/theory/uf | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 210 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 55 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_types.h | 26 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 12 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 12 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 27 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 14 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 12 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.h | 12 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 12 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 561 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 215 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 12 |
13 files changed, 770 insertions, 410 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 0ac5096d2..9b429765e 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file equality_engine.cpp ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Tianyi Liang, Tim King, Francois Bobot, Morgan Deters, Andrew Reynolds + ** Top contributors (to current version): + ** Dejan Jovanovic, Guy Katz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** @@ -42,7 +42,6 @@ EqualityEngine::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&constantTermsCount); } - /** * Data used in the BFS search through the equality graph. */ @@ -94,6 +93,8 @@ void EqualityEngine::init() { d_trueId = getNodeId(d_true); d_falseId = getNodeId(d_false); + + d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS; } EqualityEngine::~EqualityEngine() throw(AssertionException) { @@ -157,7 +158,7 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) { } void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) { - Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl; + Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << "). reason: " << candidate.reason << std::endl; if (back) { d_propagationQueue.push_back(candidate); } else { @@ -390,7 +391,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const return d_equalityNodes[nodeId]; } -void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl; @@ -408,7 +409,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, Me enqueue(MergeCandidate(t1Id, t2Id, pid, reason)); } -void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead"); assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid); @@ -421,7 +422,7 @@ void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { propagate(); } -void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; if (polarity) { // If two terms are already equal, don't assert anything @@ -889,7 +890,7 @@ void EqualityEngine::backtrack() { } -void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) { +void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason) { Debug("equality") << d_name << "::eq::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl; EqualityEdgeId edge = d_equalityEdges.size(); d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason)); @@ -920,7 +921,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const { } void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const { - Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl; + Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; // The terms must be there already Assert(hasTerm(t1) && hasTerm(t2));; @@ -933,13 +934,72 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec // Get the explanation getExplanation(t1Id, t2Id, equalities, eqp); } else { + if (eqp) { + eqp->d_id = eq::MERGED_THROUGH_TRANS; + eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t2Id]).notNode(); + } + // Get the reason for this disequality EqualityPair pair(t1Id, t2Id); Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end(), "Don't ask for stuff I didn't notify you about"); DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second; + for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { + EqualityPair toExplain = d_deducedDisequalityReasons[i]; - getExplanation(toExplain.first, toExplain.second, equalities, eqp); + EqProof* eqpc = NULL; + + // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x. + if (eqp && toExplain.first != toExplain.second) { + eqpc = new EqProof; + } + + getExplanation(toExplain.first, toExplain.second, equalities, eqpc); + + if (eqpc) { + Debug("pf::ee") << "Child proof is:" << std::endl; + eqpc->debug_print("pf::ee", 1); + + if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { + std::vector<EqProof *> orderedChildren; + bool nullCongruenceFound = false; + for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { + if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) { + + // For now, assume there can only be one null congruence child + Assert(!nullCongruenceFound); + nullCongruenceFound = true; + + Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl; + orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]); + orderedChildren.push_back(eqpc->d_children[i]->d_children[1]); + } else { + orderedChildren.push_back(eqpc->d_children[i]); + } + } + + if (nullCongruenceFound) { + eqpc->d_children = orderedChildren; + Debug("pf::ee") << "Child proof's children have been reordered. It is now:" << std::endl; + eqpc->debug_print("pf::ee", 1); + } + } + + eqp->d_children.push_back(eqpc); + } + } + + if (eqp) { + if(eqp->d_children.size() == 1) { + // The transitivity proof has just one child. Simplify. + EqProof* temp = eqp->d_children[0]; + eqp->d_children.clear(); + *eqp = *temp; + delete temp; + } + + Debug("pf::ee") << "Disequality explanation final proof: " << std::endl; + eqp->debug_print("pf::ee", 1); } } } @@ -972,7 +1032,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // If the nodes are the same, we're done if (t1Id == t2Id){ if( eqp ) { - eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]); + if ((d_nodes[t1Id].getKind() == kind::BUILTIN) && (d_nodes[t1Id].getConst<Kind>() == kind::SELECT)) { + std::vector<Node> no_children; + eqp->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, no_children); + } else { + eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]); + } } return; } @@ -1019,24 +1084,28 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl; - std::vector< EqProof * > eqp_trans; + std::vector<EqProof *> eqp_trans; // Reconstruct the path do { // The current node currentNode = bfsQueue[currentIndex].nodeId; EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId(); - MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); + unsigned reasonType = d_equalityEdges[currentEdge].getReasonType(); + Node reason = d_equalityEdges[currentEdge].getReason(); Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; + Debug("equality") << d_name << " targetNode = " << d_nodes[edgeNode] << std::endl; Debug("equality") << d_name << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; + Debug("equality") << d_name << " reason type = " << reasonType << std::endl; - EqProof * eqpc = NULL; - //make child proof if a proof is being constructed - if( eqp ){ + EqProof* eqpc = NULL; + // Make child proof if a proof is being constructed + if (eqp) { eqpc = new EqProof; eqpc->d_id = reasonType; } + // Add the actual equality to the vector switch (reasonType) { case MERGED_THROUGH_CONGRUENCE: { @@ -1044,32 +1113,47 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl; const FunctionApplication& f1 = d_applications[currentNode].original; const FunctionApplication& f2 = d_applications[edgeNode].original; + Debug("equality") << push; + Debug("equality") << "Explaining left hand side equalities" << std::endl; EqProof * eqpc1 = eqpc ? new EqProof : NULL; getExplanation(f1.a, f2.a, equalities, eqpc1); + Debug("equality") << "Explaining right hand side equalities" << std::endl; EqProof * eqpc2 = eqpc ? new EqProof : NULL; getExplanation(f1.b, f2.b, equalities, eqpc2); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); - Debug("equality-pf") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl; if( d_nodes[currentNode].getKind()==kind::EQUAL ){ //leave node null for now eqpc->d_node = Node::null(); - }else{ - Debug("equality-pf") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl; + } else { if(d_nodes[f1.a].getKind() == kind::APPLY_UF || d_nodes[f1.a].getKind() == kind::SELECT || d_nodes[f1.a].getKind() == kind::STORE) { eqpc->d_node = d_nodes[f1.a]; } else { - eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]); + if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) { + eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]); + // The first child is a PARTIAL_SELECT_0. + // Give it a child so that we know what kind of (read) it is, when we dump to LFSC. + Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0); + Assert(eqpc->d_children[0]->d_children.size() == 0); + + eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, + d_nodes[f1.b]); + } else { + eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, + ProofManager::currentPM()->mkOp(d_nodes[f1.a]), + d_nodes[f1.b]); + } } } } Debug("equality") << pop; break; } + case MERGED_THROUGH_REFLEXIVITY: { // x1 == x1 Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; @@ -1088,6 +1172,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st break; } + case MERGED_THROUGH_CONSTANTS: { // f(c1, ..., cn) = c semantically, we can just ignore it Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl; @@ -1111,23 +1196,41 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } Debug("equality") << pop; - break; } + default: { // Construct the equality - Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; - if( eqpc ){ - if(reasonType == MERGED_THROUGH_EQUALITY) { - eqpc->d_node = d_equalityEdges[currentEdge].getReason(); + Debug("equality") << d_name << "::eq::getExplanation(): adding: " + << reason << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl; + + Node a = d_nodes[currentNode]; + Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; + + if (eqpc) { + //apply proof reconstruction processing (when eqpc is non-null) + if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) { + d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b, + equalities, eqpc); + } + if (reasonType == MERGED_THROUGH_EQUALITY) { + eqpc->d_node = reason; } else { - // theory-specific proof rule - eqpc->d_node = d_nodes[d_equalityEdges[currentEdge].getNodeId()].eqNode(d_nodes[currentNode]); - Debug("equality-pf") << "theory eq : " << eqpc->d_node << std::endl; + // The LFSC translator prefers (not (= a b)) over (= (= a b) false) + + if (a == NodeManager::currentNM()->mkConst(false)) { + eqpc->d_node = b.notNode(); + } else if (b == NodeManager::currentNM()->mkConst(false)) { + eqpc->d_node = a.notNode(); + } else { + eqpc->d_node = b.eqNode(a); + } } eqpc->d_id = reasonType; } - equalities.push_back(d_equalityEdges[currentEdge].getReason()); + + equalities.push_back(reason); break; } } @@ -1137,7 +1240,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st currentIndex = bfsQueue[currentIndex].previousIndex; //---from Morgan--- - if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { + if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { if(eqpc->d_node.isNull()) { Assert(eqpc->d_children.size() == 1); EqProof *p = eqpc; @@ -1149,11 +1252,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } //---end from Morgan--- - eqp_trans.push_back( eqpc ); - + eqp_trans.push_back(eqpc); } while (currentEdge != null_id); - if(eqp) { + if (eqp) { if(eqp_trans.size() == 1) { *eqp = *eqp_trans[0]; delete eqp_trans[0]; @@ -1162,6 +1264,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); } + + eqp->debug_print("pf::ee", 1); } // Done @@ -1508,7 +1612,7 @@ void EqualityEngine::debugPrintGraph() const { EqualityEdgeId edgeId = d_equalityGraph[nodeId]; while (edgeId != null_edge) { const EqualityEdge& edge = d_equalityEdges[edgeId]; - Debug("equality::graph") << " " << d_nodes[edge.getNodeId()] << ":" << edge.getReason(); + Debug("equality::graph") << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()] << ":" << edge.getReason(); edgeId = edge.getNext(); } @@ -1517,17 +1621,19 @@ void EqualityEngine::debugPrintGraph() const { } bool EqualityEngine::areEqual(TNode t1, TNode t2) const { - Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")"; Assert(hasTerm(t1)); Assert(hasTerm(t2)); - return getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind(); + bool result = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind(); + Debug("equality") << (result ? "\t(YES)" : "\t(NO)") << std::endl; + return result; } bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const { - Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")"; // Add the terms Assert(hasTerm(t1)); @@ -1539,6 +1645,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const // If we propagated this disequality we're true if (hasPropagatedDisequality(t1Id, t2Id)) { + Debug("equality") << "\t(YES)" << std::endl; return true; } @@ -1556,6 +1663,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, t2ClassId)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } + Debug("equality") << "\t(YES)" << std::endl; return true; } @@ -1571,6 +1679,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } + Debug("equality") << "\t(YES)" << std::endl; return true; } } @@ -1587,21 +1696,33 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } + Debug("equality") << "\t(YES)" << std::endl; return true; } } // Couldn't deduce dis-equalityReturn whether the terms are disequal + Debug("equality") << "\t(NO)" << std::endl; return false; } -size_t EqualityEngine::getSize(TNode t) -{ +size_t EqualityEngine::getSize(TNode t) { // Add the term addTermInternal(t); return getEqualityNode(getEqualityNode(t).getFind()).getSize(); } + +void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) { + // Currently we can only inform one callback per trigger + Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end()); + d_pathReconstructionTriggers[trigger] = notify; +} + +unsigned EqualityEngine::getFreshMergeReasonType() { + return d_freshMergeReasonType++; +} + void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) { Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; @@ -2103,10 +2224,9 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{ d_children[i]->debug_print( c, tb+1 ); } } - Debug( c ) << ")"; + Debug( c ) << ")" << std::endl; } - } // Namespace uf } // Namespace theory } // Namespace CVC4 diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 9cfa16adf..f30f1e8a0 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -1,13 +1,13 @@ /********************* */ /*! \file equality_engine.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Tim King, Kshitij Bansal, Dejan Jovanovic, Liana Hadarean, Andrew Reynolds + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Guy Katz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** @@ -140,6 +140,18 @@ public: void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } };/* class EqualityEngineNotifyNone */ +/** + * An interface for equality engine notifications during equality path reconstruction. + * Can be used to add theory-specific logic for, e.g., proof construction. + */ +class PathReconstructionNotify { +public: + + virtual ~PathReconstructionNotify() {} + + virtual void notify(unsigned reasonType, Node reason, Node a, Node b, + std::vector<TNode>& equalities, EqProof* proof) const = 0; +}; /** * Class for keeping an incremental congruence closure over a set of terms. It provides @@ -218,6 +230,9 @@ private: /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */ KindMap d_congruenceKindsInterpreted; + /** Objects that need to be notified during equality path reconstruction */ + std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers; + /** Map from nodes to their ids */ __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; @@ -259,6 +274,9 @@ private: /** Memory for the use-list nodes */ std::vector<UseListNode> d_useListNodes; + /** A fresh merge reason type to return upon request */ + unsigned d_freshMergeReasonType; + /** * We keep a list of asserted equalities. Not among original terms, but * among the class representatives. @@ -289,7 +307,7 @@ private: // The next edge EqualityEdgeId d_nextId; // Type of reason for this equality - MergeReasonType d_mergeType; + unsigned d_mergeType; // Reason of this equality TNode d_reason; @@ -298,7 +316,7 @@ private: EqualityEdge(): d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {} - EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, MergeReasonType type, TNode reason): + EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, unsigned type, TNode reason): d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {} /** Returns the id of the next edge */ @@ -308,7 +326,7 @@ private: EqualityNodeId getNodeId() const { return d_nodeId; } /** The reason of this edge */ - MergeReasonType getReasonType() const { return d_mergeType; } + unsigned getReasonType() const { return d_mergeType; } /** The reason of this edge */ TNode getReason() const { return d_reason; } @@ -333,7 +351,7 @@ private: std::vector<EqualityEdgeId> d_equalityGraph; /** Add an edge to the equality graph */ - void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason); + void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason); /** Returns the equality node of the given node */ EqualityNode& getEqualityNode(TNode node); @@ -505,7 +523,7 @@ private: /** * Adds an equality of terms t1 and t2 to the database. */ - void assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); + void assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** * Adds a trigger equality to the database with the trigger node and polarity for notification. @@ -729,7 +747,7 @@ public: * asserting the negated predicate * @param reason the reason to keep for building explanations */ - void assertPredicate(TNode p, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); + void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** * Adds predicate p and q and makes them equal. @@ -744,7 +762,7 @@ public: * asserting the negated equality * @param reason the reason to keep for building explanations */ - void assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); + void assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** * Returns the current representative of the term t. @@ -833,6 +851,15 @@ public: */ bool consistent() const { return !d_done; } + /** + * Marks an object for merge type based notification during equality path reconstruction. + */ + void addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify); + + /** + * Returns a fresh merge reason type tag for the client to use. + */ + unsigned getFreshMergeReasonType(); }; /** @@ -876,7 +903,7 @@ class EqProof { public: EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} - MergeReasonType d_id; + unsigned d_id; Node d_node; std::vector< EqProof * > d_children; void debug_print( const char * c, unsigned tb = 0 ) const; diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index fb1e73575..346aebca7 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -1,13 +1,13 @@ /********************* */ /*! \file equality_engine_types.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds + ** Top contributors (to current version): + ** Dejan Jovanovic, Andrew Reynolds, Guy Katz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** @@ -67,14 +67,11 @@ enum MergeReasonType { MERGED_THROUGH_REFLEXIVITY, /** Equality was merged to false, due to both sides of equality being a constant */ MERGED_THROUGH_CONSTANTS, - /** (for proofs only) Equality was merged due to transitivity */ MERGED_THROUGH_TRANS, - /** Theory specific proof rules */ - MERGED_ARRAYS_ROW, - MERGED_ARRAYS_ROW1, - MERGED_ARRAYS_EXT + /** Reason types beyond this constant are theory specific reasons */ + NUMBER_OF_MERGE_REASONS }; inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { @@ -91,10 +88,10 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { case MERGED_THROUGH_CONSTANTS: out << "constants disequal"; break; - // (for proofs only) case MERGED_THROUGH_TRANS: out << "transitivity"; break; + default: out << "[theory]"; break; @@ -108,9 +105,9 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { */ struct MergeCandidate { EqualityNodeId t1Id, t2Id; - MergeReasonType type; + unsigned type; TNode reason; - MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason) + MergeCandidate(EqualityNodeId x, EqualityNodeId y, unsigned type, TNode reason) : t1Id(x), t2Id(y), type(type), reason(reason) {} }; @@ -365,4 +362,3 @@ struct TriggerInfo { } // namespace eq } // namespace theory } // namespace CVC4 - diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 4f7a2667c..ed5d99bdf 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file symmetry_breaker.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of algorithm suggested by Deharbe, Fontaine, ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011 diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 5523c1c0d..b706f340f 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -1,13 +1,13 @@ /********************* */ /*! \file symmetry_breaker.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of algorithm suggested by Deharbe, Fontaine, ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011 diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ffb537734..0c7bed773 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_uf.cpp ** \verbatim - ** Original author: Tim King - ** Major contributors: Morgan Deters, Dejan Jovanovic - ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief This is the interface to TheoryUF implementations ** @@ -105,6 +105,8 @@ void TheoryUF::check(Effort level) { TNode fact = assertion.assertion; Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl; + Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl; + if (d_thss != NULL) { bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); d_thss->assertNode(fact, isDecision); @@ -219,9 +221,15 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf); } if( pf ){ - Debug("uf-pf") << std::endl; - pf->debug_print("uf-pf"); + Debug("pf::uf") << std::endl; + pf->debug_print("pf::uf"); + } + + Debug("pf::uf") << "UF: explain( " << literal << " ):" << std::endl << "\t"; + for (unsigned i = 0; i < assumptions.size(); ++i) { + Debug("pf::uf") << assumptions[i] << " "; } + Debug("pf::uf") << std::endl; } Node TheoryUF::explain(TNode literal) { @@ -270,6 +278,7 @@ void TheoryUF::presolve() { for(vector<Node>::const_iterator i = newClauses.begin(); i != newClauses.end(); ++i) { + Debug("uf") << "uf: generating a lemma: " << *i << std::endl; d_out->lemma(*i); } } @@ -521,7 +530,7 @@ void TheoryUF::conflict(TNode a, TNode b) { } else { d_conflictNode = explain(a.eqNode(b),pf); } - ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; + ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; d_out->conflict(d_conflictNode, puf); d_conflict = true; } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index e29b923f9..42a804c09 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_uf.h ** \verbatim - ** Original author: Tim King - ** Major contributors: Dejan Jovanovic, Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief This is the interface to TheoryUF implementations ** @@ -136,7 +136,7 @@ private: * Explain a literal, with proof (if "pf" is non-NULL). */ Node explain(TNode literal, eq::EqProof* pf); - + /** Literals to propagate */ context::CDList<Node> d_literalsToPropagate; diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 6d0123a19..f6568ad7f 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_uf_model.cpp ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of Theory UF Model **/ diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 970a7d6b3..39e7ee6f0 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_uf_model.h ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Model for Theory UF **/ diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 82dacb6c2..166d11451 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_uf_rewriter.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Clark Barrett + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 3ed1c4d40..ed28cc2fc 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_uf_strong_solver.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): Clark Barrett + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of theory uf strong solver class **/ @@ -29,17 +29,44 @@ //#define LAZY_REL_EQC using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -void StrongSolverTheoryUF::SortModel::Region::addRep( Node n ) { + +namespace CVC4 { +namespace theory { +namespace uf { + +/* These are names are unambigious are we use abbreviations. */ +typedef StrongSolverTheoryUF::SortModel SortModel; +typedef SortModel::Region Region; +typedef Region::RegionNodeInfo RegionNodeInfo; +typedef RegionNodeInfo::DiseqList DiseqList; + +Region::Region(SortModel* 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::~Region() { + for(iterator i = begin(), iend = end(); i != iend; ++i) { + RegionNodeInfo* regionNodeInfo = (*i).second; + delete regionNodeInfo; + } + d_nodes.clear(); +} + +void Region::addRep( Node n ) { setRep( n, true ); } -void StrongSolverTheoryUF::SortModel::Region::takeNode( StrongSolverTheoryUF::SortModel::Region* r, Node n ){ +void Region::takeNode( Region* r, Node n ){ Assert( !hasRep( n ) ); Assert( r->hasRep( n ) ); //add representative @@ -47,8 +74,8 @@ void StrongSolverTheoryUF::SortModel::Region::takeNode( StrongSolverTheoryUF::So //take disequalities from r RegionNodeInfo* rni = r->d_nodes[n]; for( int t=0; t<2; t++ ){ - RegionNodeInfo::DiseqList* del = rni->d_disequalities[t]; - for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){ + DiseqList* del = rni->get(t); + for(DiseqList::iterator it = del->begin(); it != del->end(); ++it ){ if( (*it).second ){ r->setDisequal( n, (*it).first, t, false ); if( t==0 ){ @@ -71,21 +98,22 @@ void StrongSolverTheoryUF::SortModel::Region::takeNode( StrongSolverTheoryUF::So r->setRep( n, false ); } -void StrongSolverTheoryUF::SortModel::Region::combine( StrongSolverTheoryUF::SortModel::Region* r ){ +void Region::combine( 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 ){ + for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it) { + if( it->second->valid() ){ setRep( it->first, true ); } } - for( std::map< Node, RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){ - if( it->second->d_valid ){ + for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it){ + if( it->second->valid() ){ //take disequalities from r Node n = it->first; RegionNodeInfo* rni = it->second; for( int t=0; t<2; t++ ){ - RegionNodeInfo::DiseqList* del = rni->d_disequalities[t]; - for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){ + RegionNodeInfo::DiseqList* del = rni->get(t); + for( RegionNodeInfo::DiseqList::iterator it2 = del->begin(), + it2end = del->end(); it2 != it2end; ++it2 ){ if( (*it2).second ){ if( t==0 && hasRep( (*it2).first ) ){ setDisequal( (*it2).first, n, 0, false ); @@ -103,12 +131,12 @@ void StrongSolverTheoryUF::SortModel::Region::combine( StrongSolverTheoryUF::Sor } /** setEqual */ -void StrongSolverTheoryUF::SortModel::Region::setEqual( Node a, Node b ){ +void Region::setEqual( Node a, Node b ){ Assert( hasRep( a ) && hasRep( b ) ); //move disequalities of b over to a for( int t=0; t<2; t++ ){ - RegionNodeInfo::DiseqList* del = d_nodes[b]->d_disequalities[t]; - for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){ + DiseqList* del = d_nodes[b]->get(t); + for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){ if( (*it).second ){ Node n = (*it).first; //get the region that contains the endpoint of the disequality b != ... @@ -133,12 +161,13 @@ void StrongSolverTheoryUF::SortModel::Region::setEqual( Node a, Node b ){ setRep( b, false ); } -void StrongSolverTheoryUF::SortModel::Region::setDisequal( Node n1, Node n2, int type, bool valid ){ - //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " " << type << " " << valid << std::endl; +void Region::setDisequal( Node n1, Node n2, int type, bool valid ){ + //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " " + // << type << " " << valid << std::endl; //debugPrint("uf-ss-region-debug"); //Assert( isDisequal( n1, n2, type )!=valid ); if( isDisequal( n1, n2, type )!=valid ){ //DO_THIS: make assertion - d_nodes[ n1 ]->d_disequalities[type]->setDisequal( n2, valid ); + d_nodes[ n1 ]->get(type)->setDisequal( n2, valid ); if( type==0 ){ d_total_diseq_external = d_total_diseq_external + ( valid ? 1 : -1 ); }else{ @@ -149,7 +178,8 @@ void StrongSolverTheoryUF::SortModel::Region::setDisequal( Node n1, Node n2, int d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){ Node eq = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 ); if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){ - Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2 << std::endl; + Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2 + << std::endl; d_splits[ eq ] = false; d_splitsSize = d_splitsSize - 1; } @@ -159,20 +189,20 @@ void StrongSolverTheoryUF::SortModel::Region::setDisequal( Node n1, Node n2, int } } -void StrongSolverTheoryUF::SortModel::Region::setRep( Node n, bool valid ){ +void 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_thss->getSatContext() ); } - d_nodes[n]->d_valid = valid; + d_nodes[n]->setValid(valid); d_reps_size = d_reps_size + ( valid ? 1 : -1 ); //removing a member of the test clique from this region - if( d_testClique.find( n )!=d_testClique.end() && d_testClique[n] ){ + if( d_testClique.find( n ) != d_testClique.end() && d_testClique[n] ){ Assert( !valid ); d_testClique[n] = false; d_testCliqueSize = d_testCliqueSize - 1; //remove all splits involving n - for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){ + for( split_iterator it = begin_splits(); it != end_splits(); ++it ){ if( (*it).second ){ if( (*it).first[0]==n || (*it).first[1]==n ){ d_splits[ (*it).first ] = false; @@ -183,33 +213,41 @@ void StrongSolverTheoryUF::SortModel::Region::setRep( Node n, bool valid ){ } } -bool StrongSolverTheoryUF::SortModel::Region::isDisequal( Node n1, Node n2, int type ){ - RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->d_disequalities[type]; - return del->d_disequalities.find( n2 )!=del->d_disequalities.end() && del->d_disequalities[n2]; +bool Region::isDisequal( Node n1, Node n2, int type ) { + RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->get(type); + return del->isSet(n2) && del->getDisequalityValue(n2); } struct sortInternalDegree { - StrongSolverTheoryUF::SortModel::Region* r; - bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumInternalDisequalities()>r->d_nodes[j]->getNumInternalDisequalities());} + Region* r; + bool operator() (Node i, Node j) { + return (r->getRegionInfo(i)->getNumInternalDisequalities() > + r->getRegionInfo(j)->getNumInternalDisequalities()); + } }; struct sortExternalDegree { - StrongSolverTheoryUF::SortModel::Region* r; - bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumExternalDisequalities()>r->d_nodes[j]->getNumExternalDisequalities());} + Region* r; + bool operator() (Node i,Node j) { + return (r->getRegionInfo(i)->getNumExternalDisequalities() > + r->getRegionInfo(j)->getNumExternalDisequalities()); + } }; int gmcCount = 0; -bool StrongSolverTheoryUF::SortModel::Region::getMustCombine( int cardinality ){ +bool Region::getMustCombine( int cardinality ){ if( options::ufssRegions() && d_total_diseq_external>=unsigned(cardinality) ){ - //The number of external disequalities is greater than or equal to cardinality. - //Thus, a clique of size cardinality+1 may exist between nodes in d_regions[i] and other regions - //Check if this is actually the case: must have n nodes with outgoing degree (cardinality+1-n) for some n>0 + //The number of external disequalities is greater than or equal to + //cardinality. Thus, a clique of size cardinality+1 may exist + //between nodes in d_regions[i] and other regions Check if this is + //actually the case: must have n nodes with outgoing degree + //(cardinality+1-n) for some n>0 std::vector< int > degrees; - for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + for( Region::iterator it = begin(); it != end(); ++it ){ RegionNodeInfo* rni = it->second; - if( rni->d_valid ){ - if( rni->getNumDisequalities()>=cardinality ){ + if( rni->valid() ){ + if( rni->getNumDisequalities() >= cardinality ){ int outDeg = rni->getNumExternalDisequalities(); if( outDeg>=cardinality ){ //we have 1 node of degree greater than (cardinality) @@ -226,7 +264,8 @@ bool StrongSolverTheoryUF::SortModel::Region::getMustCombine( int cardinality ){ } gmcCount++; if( gmcCount%100==0 ){ - Trace("gmc-count") << gmcCount << " " << cardinality << " sample : " << degrees.size() << std::endl; + Trace("gmc-count") << gmcCount << " " << cardinality + << " sample : " << degrees.size() << std::endl; } //this should happen relatively infrequently.... std::sort( degrees.begin(), degrees.end() ); @@ -239,13 +278,14 @@ bool StrongSolverTheoryUF::SortModel::Region::getMustCombine( int cardinality ){ return false; } -bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){ +bool Region::check( Theory::Effort level, int cardinality, + std::vector< Node >& clique ) { if( d_reps_size>unsigned(cardinality) ){ if( d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){ 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 ){ + for( iterator it = begin(); it != end(); ++it ){ + if( it->second->valid() ){ clique.push_back( it->first ); } } @@ -254,15 +294,19 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c }else{ return false; } - }else if( options::ufssRegions() || options::ufssEagerSplits() || level==Theory::EFFORT_FULL ){ + }else if( options::ufssRegions() || options::ufssEagerSplits() || + level==Theory::EFFORT_FULL ) { //build test clique, up to size cardinality+1 if( d_testCliqueSize<=unsigned(cardinality) ){ std::vector< Node > newClique; if( d_testCliqueSize<unsigned(cardinality) ){ - for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + for( iterator it = begin(); it != end(); ++it ){ //if not in the test clique, add it to the set of new members - if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){ - //if( it->second->getNumInternalDisequalities()>cardinality || level==Theory::EFFORT_FULL ){ + if( it->second->valid() && + ( d_testClique.find( it->first ) == d_testClique.end() || + !d_testClique[ it->first ] ) ){ + //if( it->second->getNumInternalDisequalities()>cardinality || + // level==Theory::EFFORT_FULL ){ newClique.push_back( it->first ); //} } @@ -271,14 +315,18 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c sortInternalDegree sidObj; sidObj.r = this; std::sort( newClique.begin(), newClique.end(), sidObj ); - newClique.erase( newClique.begin() + ( cardinality - d_testCliqueSize ) + 1, newClique.end() ); + int offset = ( cardinality - d_testCliqueSize ) + 1; + newClique.erase( newClique.begin() + offset, newClique.end() ); }else{ //scan for the highest degree int maxDeg = -1; Node maxNode; - for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ + for( std::map< Node, RegionNodeInfo* >::iterator + it = d_nodes.begin(); it != d_nodes.end(); ++it ){ //if not in the test clique, add it to the set of new members - if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){ + if( it->second->valid() && + ( d_testClique.find( it->first )==d_testClique.end() || + !d_testClique[ it->first ] ) ){ if( it->second->getNumInternalDisequalities()>maxDeg ){ maxDeg = it->second->getNumInternalDisequalities(); maxNode = it->first; @@ -290,18 +338,27 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c } //check splits internal to new members for( int j=0; j<(int)newClique.size(); j++ ){ - Debug("uf-ss-debug") << "Choose to add clique member " << newClique[j] << std::endl; + Debug("uf-ss-debug") << "Choose to add clique member " + << newClique[j] << std::endl; for( int k=(j+1); k<(int)newClique.size(); k++ ){ if( !isDisequal( newClique[j], newClique[k], 1 ) ){ - d_splits[ NodeManager::currentNM()->mkNode( EQUAL, newClique[j], newClique[k] ) ] = true; + Node at_j = newClique[j]; + Node at_k = newClique[k]; + Node j_eq_k = + NodeManager::currentNM()->mkNode( EQUAL, at_j, at_k ); + d_splits[ j_eq_k ] = true; d_splitsSize = d_splitsSize + 1; } } //check disequalities with old members - for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){ + for( NodeBoolMap::iterator it = d_testClique.begin(); + it != d_testClique.end(); ++it ){ if( (*it).second ){ if( !isDisequal( (*it).first, newClique[j], 1 ) ){ - d_splits[ NodeManager::currentNM()->mkNode( EQUAL, (*it).first, newClique[j] ) ] = true; + Node at_it = (*it).first; + Node at_j = newClique[j]; + Node it_eq_j = at_it.eqNode(at_j); + d_splits[ it_eq_j ] = true; d_splitsSize = d_splitsSize + 1; } } @@ -313,10 +370,12 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c d_testCliqueSize = d_testCliqueSize + 1; } } - //check if test clique has larger size than cardinality, and forms a clique - if( d_testCliqueSize>=unsigned(cardinality+1) && d_splitsSize==0 ){ + // Check if test clique has larger size than cardinality, and + // forms a clique. + if( d_testCliqueSize >= unsigned(cardinality+1) && d_splitsSize==0 ){ //test clique is a clique - for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){ + for( NodeBoolMap::iterator it = d_testClique.begin(); + it != d_testClique.end(); ++it ){ if( (*it).second ){ clique.push_back( (*it).first ); } @@ -328,10 +387,12 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c return false; } -bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) { +bool Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) +{ if( d_testCliqueSize>=unsigned(cardinality+1) ){ //test clique is a clique - for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){ + for( NodeBoolMap::iterator it = d_testClique.begin(); + it != d_testClique.end(); ++it ){ if( (*it).second ){ clique.push_back( (*it).first ); } @@ -341,12 +402,13 @@ bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinalit return false; } -void StrongSolverTheoryUF::SortModel::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){ - for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ +void Region::getNumExternalDisequalities( + std::map< Node, int >& num_ext_disequalities ){ + for( Region::iterator it = begin(); it != end(); ++it ){ RegionNodeInfo* rni = it->second; - if( rni->d_valid ){ - RegionNodeInfo::DiseqList* del = rni->d_disequalities[0]; - for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){ + if( rni->valid() ){ + DiseqList* del = rni->get(0); + for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){ if( (*it2).second ){ num_ext_disequalities[ (*it2).first ]++; } @@ -355,32 +417,35 @@ void StrongSolverTheoryUF::SortModel::Region::getNumExternalDisequalities( std:: } } -void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool incClique ){ +void 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 ){ + for( Region::iterator it = begin(); it != end(); ++it ){ RegionNodeInfo* rni = it->second; - if( rni->d_valid ){ + if( rni->valid() ){ Node n = it->first; Debug( c ) << " " << n << std::endl; for( int i=0; i<2; i++ ){ Debug( c ) << " " << ( i==0 ? "Ext" : "Int" ) << " disequal:"; - RegionNodeInfo::DiseqList* del = rni->d_disequalities[i]; - for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){ + DiseqList* del = rni->get(i); + for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){ if( (*it2).second ){ Debug( c ) << " " << (*it2).first; } } - Debug( c ) << ", total = " << del->d_size << std::endl; + Debug( c ) << ", total = " << del->size() << std::endl; } } } - Debug( c ) << "Total disequal: " << d_total_diseq_external << " external," << std::endl; - Debug( c ) << " " << d_total_diseq_internal<< " internal." << std::endl; + Debug( c ) << "Total disequal: " << d_total_diseq_external << " external," + << std::endl; + Debug( c ) << " " << d_total_diseq_internal << " internal." + << std::endl; if( incClique ){ Debug( c ) << "Candidate clique members: " << std::endl; Debug( c ) << " "; - for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++ it ){ + for( NodeBoolMap::iterator it = d_testClique.begin(); + it != d_testClique.end(); ++ it ){ if( (*it).second ){ Debug( c ) << (*it).first << " "; } @@ -388,7 +453,8 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in Debug( c ) << ", size = " << d_testCliqueSize << std::endl; Debug( c ) << "Required splits: " << std::endl; Debug( c ) << " "; - for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++ it ){ + for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); + ++ it ){ if( (*it).second ){ Debug( c ) << (*it).first << " "; } @@ -397,17 +463,25 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in } } - - - - - - - -StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ), - d_thss( thss ), 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( u, 0 ), - d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){ +SortModel::SortModel( Node n, + context::Context* c, + context::UserContext* u, + StrongSolverTheoryUF* thss ) + : d_type( n.getType() ) + , d_thss( thss ) + , 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( u, 0 ) + , d_hasCard( c, false ) + , d_maxNegCard( c, 0 ) + , d_initialized( u, false ) + , d_lemma_cache( u ) +{ d_cardinality_term = n; //if( d_type.isSort() ){ // TypeEnumerator te(tn); @@ -417,8 +491,17 @@ StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context //} } +SortModel::~SortModel() { + for(std::vector<Region*>::iterator i = d_regions.begin(); + i != d_regions.end(); ++i) { + Region* region = *i; + delete region; + } + d_regions.clear(); +} + /** initialize */ -void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){ +void SortModel::initialize( OutputChannel* out ){ if( !d_initialized ){ d_initialized = true; allocateCardinality( out ); @@ -426,17 +509,20 @@ void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){ } /** new node */ -void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){ +void SortModel::newEqClass( Node n ){ if( !d_conflict ){ if( d_regions_map.find( n )==d_regions_map.end() ){ - //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 ){ + // 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_thss->getOutputChannel() ); } } if( options::ufssTotality() ){ - //regions map will store whether we need to equate this term with a constant equivalence class + // 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{ @@ -444,16 +530,20 @@ void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){ } }else{ if( !options::ufssRegions() ){ - //if not using regions, always add new equivalence classes to region index = 0 + // 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; + 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 ); + d_regions[ d_regions_index ]->setValid(true); + Assert( !options::ufssRegions() || + d_regions[ d_regions_index ]->getNumReps()==0 ); }else{ d_regions.push_back( new Region( this, d_thss->getSatContext() ) ); } @@ -466,7 +556,7 @@ void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){ } /** merge */ -void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){ +void SortModel::merge( Node a, Node b ){ if( !d_conflict ){ if( options::ufssTotality() ){ if( d_regions_map[b]==-1 ){ @@ -476,7 +566,8 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){ }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; + 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() ); @@ -493,10 +584,15 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){ 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 + // Either move a to d_regions[bi], or b to d_regions[ai]. + RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a); + RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b); + int aex = ( a_region_info->getNumInternalDisequalities() - + getNumDisequalitiesToRegion( a, bi ) ); + int bex = ( b_region_info->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 ); @@ -529,7 +625,7 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){ } /** assert terms are disequal */ -void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reason ){ +void SortModel::assertDisequal( Node a, Node b, Node reason ){ if( !d_conflict ){ if( options::ufssTotality() ){ //do nothing @@ -584,7 +680,7 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso } } -bool StrongSolverTheoryUF::SortModel::areDisequal( Node a, Node b ) { +bool SortModel::areDisequal( Node a, Node b ) { Assert( a == d_thss->getTheory()->d_equalityEngine.getRepresentative( a ) ); Assert( b == d_thss->getTheory()->d_equalityEngine.getRepresentative( b ) ); if( d_regions_map.find( a )!=d_regions_map.end() && @@ -598,7 +694,7 @@ bool StrongSolverTheoryUF::SortModel::areDisequal( Node a, Node b ) { } /** check */ -void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel* out ){ +void SortModel::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; @@ -616,7 +712,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel if( !options::ufssTotality() ){ //do a check within each region for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ + if( d_regions[i]->valid() ){ std::vector< Node > clique; if( d_regions[i]->check( level, d_cardinality, clique ) ){ if( options::ufssMode()==UF_SS_FULL ){ @@ -637,7 +733,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel 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( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){ //just add the clique lemma if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){ std::vector< Node > clique; @@ -661,18 +757,19 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel } } } - //if no added lemmas, force continuation via combination of regions + //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; + Trace("uf-ss-debug") << "No splits added. " << d_cardinality + << std::endl; Trace("uf-ss-si") << "Must combine region" << std::endl; bool recheck = false; if( options::sortInference()){ - //if sort inference is enabled, search for regions with same sort + //If sort inference is enabled, search for regions with same sort. std::map< int, int > sortsFound; for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ - Node op = d_regions[i]->d_nodes.begin()->first; + if( d_regions[i]->valid() ){ + Node op = d_regions[i]->frontKey(); int sort_id = d_thss->getSortInference()->getSortId(op); if( sortsFound.find( sort_id )!=sortsFound.end() ){ combineRegions( sortsFound[sort_id], i ); @@ -687,7 +784,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel if( !recheck ) { //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 ){ + if( d_regions[i]->valid() ){ int fcr = forceCombineRegion( i, false ); Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl; if( options::ufssMode()==UF_SS_FULL || fcr!=-1 ){ @@ -708,26 +805,28 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel } } -void StrongSolverTheoryUF::SortModel::presolve() { +void SortModel::presolve() { d_initialized = false; d_aloc_cardinality = 0; } -void StrongSolverTheoryUF::SortModel::propagate( Theory::Effort level, OutputChannel* out ){ +void SortModel::propagate( Theory::Effort level, OutputChannel* out ){ } -Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){ +Node SortModel::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() ){ + bool value; + if( !d_thss->getTheory()->d_valuation.hasSatValue( cn, value ) ){ Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl; return cn; }else{ - Trace("uf-ss-dec-debug") << " dec : " << cn << " already asserted " << d_cardinality_assertions[cn].get() << std::endl; + Trace("uf-ss-dec-debug") << " dec : " << cn << " already asserted " << value << std::endl; + Assert( !value ); } } } @@ -737,7 +836,7 @@ Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){ return Node::null(); } -bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* m ){ +bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){ if( options::ufssTotality() ){ //do nothing }else{ @@ -774,7 +873,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* // 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( d_regions[i]->valid() ){ if( validRegionIndex!=-1 ){ combineRegions( validRegionIndex, i ); if( addSplit( d_regions[validRegionIndex], out )!=0 ){ @@ -798,11 +897,11 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* } -int StrongSolverTheoryUF::SortModel::getNumDisequalitiesToRegion( Node n, int ri ){ +int SortModel::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 ){ + DiseqList* del = d_regions[ni]->getRegionInfo(n)->get(0); + for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){ if( (*it).second ){ if( d_regions_map[ (*it).first ]==ri ){ counter++; @@ -812,12 +911,14 @@ int StrongSolverTheoryUF::SortModel::getNumDisequalitiesToRegion( Node n, int ri return counter; } -void StrongSolverTheoryUF::SortModel::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 ){ +void SortModel::getDisequalitiesToRegions(int ri, + std::map< int, int >& regions_diseq) +{ + Region* region = d_regions[ri]; + for(Region::iterator it = region->begin(); it != region->end(); ++it ){ + if( it->second->valid() ){ + DiseqList* del = it->second->get(0); + for( DiseqList::iterator it2 = del->begin(); it2 != del->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; @@ -828,7 +929,7 @@ void StrongSolverTheoryUF::SortModel::getDisequalitiesToRegions( int ri, std::ma } } -void StrongSolverTheoryUF::SortModel::setSplitScore( Node n, int s ){ +void SortModel::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; @@ -840,13 +941,13 @@ void StrongSolverTheoryUF::SortModel::setSplitScore( Node n, int s ){ } } -void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ +void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ if( !d_conflict ){ - Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = "; - Trace("uf-ss-assert") << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl; + Trace("uf-ss-assert") + << "Assert cardinality "<< d_type << " " << c << " " << val << " level = " + << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl; Assert( c>0 ); Node cl = getCardinalityLiteral( c ); - d_cardinality_assertions[ cl ] = val; if( val ){ bool doCheckRegions = !d_hasCard; bool prevHasCard = d_hasCard; @@ -861,7 +962,7 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int //should check all regions now if( doCheckRegions ){ for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ + if( d_regions[i]->valid() ){ checkRegion( i ); if( d_conflict ){ return; @@ -890,8 +991,9 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int bool needsCard = true; for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){ if( it->first<=d_aloc_cardinality.get() ){ - if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){ - Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl; + bool value; + if( !d_thss->getTheory()->d_valuation.hasSatValue( it->second, value ) ){ + Debug("fmf-card-debug") << "..does not need allocate because we are waiting for " << it->second << std::endl; needsCard = false; break; } @@ -912,7 +1014,7 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int } } -void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){ +void SortModel::checkRegion( int ri, bool checkCombine ){ if( isValid(ri) && d_hasCard ){ Assert( d_cardinality>0 ); if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){ @@ -941,10 +1043,10 @@ void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){ } } -int StrongSolverTheoryUF::SortModel::forceCombineRegion( int ri, bool useDensity ){ +int SortModel::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 ){ + if( ri!=i && d_regions[i]->valid() ){ return combineRegions( ri, i ); } } @@ -981,7 +1083,7 @@ int StrongSolverTheoryUF::SortModel::forceCombineRegion( int ri, bool useDensity } -int StrongSolverTheoryUF::SortModel::combineRegions( int ai, int bi ){ +int SortModel::combineRegions( int ai, int bi ){ #ifdef COMBINE_REGIONS_SMALL_INTO_LARGE if( d_regions[ai]->getNumReps()<d_regions[bi]->getNumReps() ){ return combineRegions( bi, ai ); @@ -989,19 +1091,20 @@ int StrongSolverTheoryUF::SortModel::combineRegions( int ai, int bi ){ #endif Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl; Assert( isValid( ai ) && isValid( bi ) ); - for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[bi]->d_nodes.begin(); it != d_regions[bi]->d_nodes.end(); ++it ){ + Region* region_bi = d_regions[bi]; + for(Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it){ Region::RegionNodeInfo* rni = it->second; - if( rni->d_valid ){ + if( rni->valid() ){ d_regions_map[ it->first ] = ai; } } //update regions disequal DO_THIS? d_regions[ai]->combine( d_regions[bi] ); - d_regions[bi]->d_valid = false; + d_regions[bi]->setValid( false ); return ai; } -void StrongSolverTheoryUF::SortModel::moveNode( Node n, int ri ){ +void SortModel::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 ) ); @@ -1010,7 +1113,7 @@ void StrongSolverTheoryUF::SortModel::moveNode( Node n, int ri ){ d_regions_map[n] = ri; } -void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ +void SortModel::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; } @@ -1028,20 +1131,26 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ //allocate the lowest such that it is not asserted Node cl; + bool increment; do { + increment = false; d_aloc_cardinality = d_aloc_cardinality + 1; cl = getCardinalityLiteral( d_aloc_cardinality ); - }while( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() && !d_cardinality_assertions[cl] ); - //if one is already asserted postively, abort - if( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() ){ - return; - } + bool value; + if( d_thss->getTheory()->d_valuation.hasSatValue( cl, value ) ){ + if( value ){ + //if one is already asserted postively, abort + return; + }else{ + increment = true; + } + } + }while( increment ); //check for abort case if( options::ufssAbortCardinality()==d_aloc_cardinality ){ - //abort here DO_THIS Message() << "Maximum cardinality reached." << std::endl; - exit( 0 ); + exit( 1 ); }else{ if( applyTotality( d_aloc_cardinality ) ){ //must generate new cardinality lemma term @@ -1093,11 +1202,12 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ } } -int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ +int SortModel::addSplit( Region* r, OutputChannel* out ){ Node s; if( r->hasSplits() ){ //take the first split you find - for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){ + for( Region::split_iterator it = r->begin_splits(); + it != r->end_splits(); ++it ){ if( (*it).second ){ s = (*it).first; break; @@ -1106,13 +1216,16 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ Assert( s!=Node::null() ); }else{ if( options::ufssMode()!=UF_SS_FULL ){ - //since candidate clique is not reported, we may need to find splits manually - for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){ - if ( it->second->d_valid ){ - for ( std::map< Node, Region::RegionNodeInfo* >::iterator it2 = r->d_nodes.begin(); it2 != r->d_nodes.end(); ++it2 ){ - if ( it->second!=it2->second && it2->second->d_valid ){ + // Since candidate clique is not reported, we may need to find + // splits manually. + for ( Region::iterator it = r->begin(); it != r->end(); ++it ){ + if ( it->second->valid() ){ + for ( Region::iterator it2 = r->begin(); it2 != r->end(); ++it2 ){ + if ( it->second!=it2->second && it2->second->valid() ){ if( !r->isDisequal( it->first, it2->first, 1 ) ){ - s = NodeManager::currentNM()->mkNode( EQUAL, it->first, it2->first ); + Node it_node = it->first; + Node it2_node = it2->first; + s = it_node.eqNode(it2_node); } } } @@ -1128,7 +1241,8 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ Node b_t = NodeManager::currentNM()->mkConst( true ); Node b_f = NodeManager::currentNM()->mkConst( false ); if( ss==b_f ){ - Trace("uf-ss-lemma") << "....Assert disequal directly : " << s[0] << " " << s[1] << std::endl; + Trace("uf-ss-lemma") << "....Assert disequal directly : " + << s[0] << " " << s[1] << std::endl; assertDisequal( s[0], s[1], b_t ); return -1; }else{ @@ -1165,7 +1279,7 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ } -void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){ +void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){ Assert( d_hasCard ); Assert( d_cardinality>0 ); while( clique.size()>size_t(d_cardinality+1) ){ @@ -1318,7 +1432,7 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu } } -void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){ +void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){ if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){ if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){ d_totality_lems[n].push_back( cardinality ); @@ -1346,7 +1460,7 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){ eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) ); } - Node ax = NodeManager::currentNM()->mkNode( OR, eqs ); + Node ax = eqs.size()==1 ? eqs[0] : NodeManager::currentNM()->mkNode( OR, eqs ); Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax ); Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl; d_thss->getOutputChannel().lemma( lem ); @@ -1369,7 +1483,7 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, } } -void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& clique ) { +void SortModel::addClique( int c, std::vector< Node >& clique ) { //if( d_clique_trie[c].add( clique ) ){ // d_cliques[ c ].push_back( clique ); //} @@ -1377,20 +1491,20 @@ void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& cli /** apply totality */ -bool StrongSolverTheoryUF::SortModel::applyTotality( int cardinality ){ +bool SortModel::applyTotality( int cardinality ){ return options::ufssTotality() || cardinality<=options::ufssTotalityLimited(); // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() ); } /** get totality lemma terms */ -Node StrongSolverTheoryUF::SortModel::getTotalityLemmaTerm( int cardinality, int i ){ +Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){ return d_totality_terms[0][i]; //}else{ // return d_totality_terms[cardinality][i]; //} } -void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() { +void SortModel::simpleCheckCardinality() { if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()<d_maxNegCard.get() ){ Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ), getCardinalityLiteral( d_maxNegCard.get() ).negate() ); @@ -1400,7 +1514,7 @@ void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() { } } -bool StrongSolverTheoryUF::SortModel::doSendLemma( Node lem ) { +bool SortModel::doSendLemma( Node lem ) { if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){ d_lemma_cache[lem] = true; d_thss->getOutputChannel().lemma( lem ); @@ -1410,32 +1524,36 @@ bool StrongSolverTheoryUF::SortModel::doSendLemma( Node lem ) { } } -void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){ +void SortModel::debugPrint( const char* c ){ Debug( c ) << "-- Conflict Find:" << std::endl; Debug( c ) << "Number of reps = " << d_reps << std::endl; Debug( c ) << "Cardinality req = " << d_cardinality << std::endl; unsigned debugReps = 0; for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ + Region* region = d_regions[i]; + if( region->valid() ){ Debug( c ) << "Region #" << i << ": " << std::endl; - d_regions[i]->debugPrint( c, true ); + region->debugPrint( c, true ); Debug( c ) << std::endl; - for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[i]->d_nodes.begin(); it != d_regions[i]->d_nodes.end(); ++it ){ - if( it->second->d_valid ){ + for( Region::iterator it = region->begin(); it != region->end(); ++it ){ + if( it->second->valid() ){ if( d_regions_map[ it->first ]!=i ){ - Debug( c ) << "***Bad regions map : " << it->first << " " << d_regions_map[ it->first ].get() << std::endl; + Debug( c ) << "***Bad regions map : " << it->first + << " " << d_regions_map[ it->first ].get() << std::endl; } } } - debugReps += d_regions[i]->getNumReps(); + debugReps += region->getNumReps(); } } + if( debugReps!=d_reps ){ - Debug( c ) << "***Bad reps: " << d_reps << ", actual = " << debugReps << std::endl; + Debug( c ) << "***Bad reps: " << d_reps << ", " + << "actual = " << debugReps << std::endl; } } -bool StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){ +bool SortModel::debugModel( TheoryModel* m ){ if( Trace.isOn("uf-ss-warn") ){ std::vector< Node > eqcs; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine ); @@ -1503,27 +1621,42 @@ bool StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){ return true; } -int StrongSolverTheoryUF::SortModel::getNumRegions(){ +int SortModel::getNumRegions(){ int count = 0; for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ + if( d_regions[i]->valid() ){ count++; } } return count; } -Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) { - if( d_cardinality_literal.find( c )==d_cardinality_literal.end() ){ - d_cardinality_literal[c] = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_term, - NodeManager::currentNM()->mkConst( Rational( c ) ) ); +Node SortModel::getCardinalityLiteral( int c ) { + if( d_cardinality_literal.find(c) == d_cardinality_literal.end() ){ + Node c_as_rational = NodeManager::currentNM()->mkConst(Rational(c)); + d_cardinality_literal[c] = + NodeManager::currentNM()->mkNode(CARDINALITY_CONSTRAINT, + d_cardinality_term, + c_as_rational); + } return d_cardinality_literal[c]; } -StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : -d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ), d_min_pos_com_card( c, -1 ), -d_card_assertions_eqv_lemma( u ), d_min_pos_tn_master_card( c, -1 ), d_rel_eqc( c ) +StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, + context::UserContext* u, + OutputChannel& out, + TheoryUF* th) + : d_out( &out ) + , d_th( th ) + , d_conflict( c, false ) + , d_rep_model() + , d_aloc_com_card( u, 0 ) + , d_com_card_assertions( c ) + , d_min_pos_com_card( c, -1 ) + , d_card_assertions_eqv_lemma( u ) + , d_min_pos_tn_master_card( c, -1 ) + , d_rel_eqc( c ) { if( options::ufssDiseqPropagation() ){ d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this ); @@ -1899,7 +2032,7 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ //} -StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ +SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ TypeNode tn = n.getType(); std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn ); //pre-register the type if not done already @@ -1914,9 +2047,7 @@ StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ } } -void StrongSolverTheoryUF::notifyRestart(){ - -} +void StrongSolverTheoryUF::notifyRestart(){} /** get cardinality for sort */ int StrongSolverTheoryUF::getCardinality( Node n ) { @@ -2021,27 +2152,31 @@ void StrongSolverTheoryUF::checkCombinedCardinality() { conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) ); conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() ); Node cf = NodeManager::currentNM()->mkNode( AND, conf ); - Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict : " << cf << std::endl; - Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict : " << cf << std::endl; + Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict" + << " : " << cf << std::endl; + Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict" + << " : " << cf << std::endl; getOutputChannel().conflict( cf ); d_conflict.set( true ); return; } } - if( d_min_pos_com_card.get()!=-1 && totalCombinedCard>d_min_pos_com_card.get() ){ + int cc = d_min_pos_com_card.get(); + if( cc !=-1 && totalCombinedCard > cc ){ //conflict - int cc = d_min_pos_com_card.get(); - Assert( d_com_card_literal.find( cc )!=d_com_card_literal.end() ); + Assert( d_com_card_literal.find( cc ) != d_com_card_literal.end() ); Node com_lit = d_com_card_literal[cc]; - Assert( d_com_card_assertions.find( com_lit )!=d_com_card_assertions.end() ); + Assert(d_com_card_assertions.find(com_lit)!=d_com_card_assertions.end()); Assert( d_com_card_assertions[com_lit] ); std::vector< Node > conf; conf.push_back( com_lit ); int totalAdded = 0; - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); + it != d_rep_model.end(); ++it ){ bool doAdd = true; if( options::ufssFairnessMonotone() ){ - std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first ); + std::map< TypeNode, bool >::iterator its = + d_tn_mono_slave.find( it->first ); if( its!=d_tn_mono_slave.end() && its->second ){ doAdd = false; } @@ -2058,8 +2193,10 @@ void StrongSolverTheoryUF::checkCombinedCardinality() { } } Node cf = NodeManager::currentNM()->mkNode( AND, conf ); - Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf << std::endl; - Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf << std::endl; + Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf + << std::endl; + Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf + << std::endl; getOutputChannel().conflict( cf ); d_conflict.set( true ); } @@ -2113,8 +2250,10 @@ StrongSolverTheoryUF::Statistics::~Statistics(){ } -DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss) : - d_qe(qe), d_ufss(ufss){ +DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe, + StrongSolverTheoryUF* ufss) + : d_qe(qe), d_ufss(ufss) +{ d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); } @@ -2182,3 +2321,7 @@ DisequalityPropagator::Statistics::Statistics(): DisequalityPropagator::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(& d_propagations); } + +}/* CVC4::theory namespace::uf */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index db4c50423..11f0664f3 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_uf_strong_solver.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Theory uf strong solver **/ @@ -25,17 +25,19 @@ #include "util/statistics_registry.h" namespace CVC4 { - class SortInference; - namespace theory { - class SubsortSymmetryBreaker; - namespace uf { - class TheoryUF; class DisequalityPropagator; +} /* namespace CVC4::theory::uf */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ + +namespace CVC4 { +namespace theory { +namespace uf { class StrongSolverTheoryUF{ protected: @@ -44,83 +46,135 @@ protected: typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap; public: - /** information for incremental conflict/clique finding for a particular sort */ + /** + * Information for incremental conflict/clique finding for a + * particular sort. + */ class SortModel { private: std::map< Node, std::vector< int > > d_totality_lems; std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms; std::map< Node, int > d_sym_break_index; public: - /** a partition of the current equality graph for which cliques can occur internally */ + + /** + * A partition of the current equality graph for which cliques + * can occur internally. + */ class Region { public: - /** conflict find pointer */ - SortModel* d_cf; /** information stored about each node in region */ class RegionNodeInfo { public: /** disequality list for node */ class DiseqList { public: - DiseqList( context::Context* c ) : d_size( c, 0 ), d_disequalities( c ){} + DiseqList( context::Context* c ) + : d_size( c, 0 ), d_disequalities( c ) {} ~DiseqList(){} - context::CDO< unsigned > d_size; - NodeBoolMap d_disequalities; + void setDisequal( Node n, bool valid ){ - Assert( d_disequalities.find( n )==d_disequalities.end() || d_disequalities[n]!=valid ); + Assert( (!isSet(n)) || getDisequalityValue(n) != valid ); d_disequalities[ n ] = valid; d_size = d_size + ( valid ? 1 : -1 ); } - }; - private: - DiseqList d_internal; - DiseqList d_external; + bool isSet(Node n) const { + return d_disequalities.find(n) != d_disequalities.end(); + } + bool getDisequalityValue(Node n) const { + Assert(isSet(n)); + return (*(d_disequalities.find(n))).second; + } + + int size() const { return d_size; } + + typedef NodeBoolMap::iterator iterator; + iterator begin() { return d_disequalities.begin(); } + iterator end() { return d_disequalities.end(); } + + private: + context::CDO< int > d_size; + NodeBoolMap d_disequalities; + }; /* class DiseqList */ public: /** constructor */ - RegionNodeInfo( context::Context* c ) : - d_internal( c ), d_external( c ), d_valid( c, true ){ + RegionNodeInfo( context::Context* c ) + : d_internal(c), d_external(c), d_valid(c, true) { d_disequalities[0] = &d_internal; d_disequalities[1] = &d_external; } ~RegionNodeInfo(){} + + int getNumDisequalities() const { + return d_disequalities[0]->size() + d_disequalities[1]->size(); + } + int getNumExternalDisequalities() const { + return d_disequalities[0]->size(); + } + int getNumInternalDisequalities() const { + return d_disequalities[1]->size(); + } + + bool valid() const { return d_valid; } + void setValid(bool valid) { d_valid = valid; } + + DiseqList* get(unsigned i) { return d_disequalities[i]; } + + private: + DiseqList d_internal; + DiseqList d_external; context::CDO< bool > d_valid; DiseqList* d_disequalities[2]; + }; /* class RegionNodeInfo */ - int getNumDisequalities() { return d_disequalities[0]->d_size + d_disequalities[1]->d_size; } - int getNumExternalDisequalities() { return d_disequalities[0]->d_size; } - int getNumInternalDisequalities() { return d_disequalities[1]->d_size; } - }; - ///** end class RegionNodeInfo */ private: + /** conflict find pointer */ + SortModel* d_cf; + context::CDO< unsigned > d_testCliqueSize; context::CDO< unsigned > d_splitsSize; - public: //a postulated clique NodeBoolMap d_testClique; //disequalities needed for this clique to happen NodeBoolMap d_splits; - private: //number of valid representatives in this region context::CDO< unsigned > d_reps_size; //total disequality size (external) context::CDO< unsigned > d_total_diseq_external; //total disequality size (internal) context::CDO< unsigned > d_total_diseq_internal; - private: /** set rep */ void setRep( Node n, bool valid ); - public: - //constructor - Region( SortModel* 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 ) { - } - virtual ~Region(){} //region node infomation std::map< Node, RegionNodeInfo* > d_nodes; //whether region is valid context::CDO< bool > d_valid; + public: + //constructor + Region( SortModel* cf, context::Context* c ); + virtual ~Region(); + + typedef std::map< Node, RegionNodeInfo* >::iterator iterator; + iterator begin() { return d_nodes.begin(); } + iterator end() { return d_nodes.end(); } + + typedef NodeBoolMap::iterator split_iterator; + split_iterator begin_splits() { return d_splits.begin(); } + split_iterator end_splits() { return d_splits.end(); } + + /** Returns a RegionInfo. */ + RegionNodeInfo* getRegionInfo(Node n) { + Assert(d_nodes.find(n) != d_nodes.end()); + return (* (d_nodes.find(n))).second; + } + + /** Returns whether or not d_valid is set in current context. */ + bool valid() const { return d_valid; } + + /** Sets d_valid to the value valid in the current context.*/ + void setValid(bool valid) { d_valid = valid; } + /** add rep */ void addRep( Node n ); //take node from region @@ -131,13 +185,14 @@ public: void setEqual( Node a, Node b ); //set n1 != n2 to value 'valid', type is whether it is internal/external void setDisequal( Node n1, Node n2, int type, bool valid ); - public: //get num reps int getNumReps() { return d_reps_size; } //get test clique size int getTestCliqueSize() { return d_testCliqueSize; } // has representative - bool hasRep( Node n ) { return d_nodes.find( n )!=d_nodes.end() && d_nodes[n]->d_valid; } + bool hasRep( Node n ) { + return d_nodes.find(n) != d_nodes.end() && d_nodes[n]->valid(); + } // is disequal bool isDisequal( Node n1, Node n2, int type ); /** get must merge */ @@ -145,15 +200,18 @@ public: /** has splits */ bool hasSplits() { return d_splitsSize>0; } /** get external disequalities */ - void getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ); - public: + void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities ); /** check for cliques */ bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique ); /** get candidate clique */ bool getCandidateClique( int cardinality, std::vector< Node >& clique ); //print debug void debugPrint( const char* c, bool incClique = false ); - }; + + // Returns the first key in d_nodes. + Node frontKey() const { return d_nodes.begin()->first; } + }; /* class Region */ + private: /** the type this model is for */ TypeNode d_type; @@ -173,16 +231,17 @@ public: std::vector< Node > d_disequalities; /** number of representatives in all regions */ context::CDO< unsigned > d_reps; - 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 ); /** is valid */ - bool isValid( int ri ) { return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->d_valid; } + bool isValid( int ri ) { + return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->valid(); + } /** set split score */ void setSplitScore( Node n, int s ); - private: /** check if we need to combine region ri */ void checkRegion( int ri, bool checkCombine = true ); /** force combine region */ @@ -191,18 +250,21 @@ public: int combineRegions( int ai, int bi ); /** move node n to region ri */ void moveNode( Node n, int ri ); - private: /** allocate cardinality */ void allocateCardinality( OutputChannel* out ); - /** add split 0 = no split, -1 = entailed disequality added, 1 = split added */ + /** + * Add splits. Returns + * 0 = no split, + * -1 = entailed disequality added, or + * 1 = split added. + */ int 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: + class NodeTrie { - std::map< Node, NodeTrie > d_children; public: bool add( std::vector< Node >& n, unsigned i = 0 ){ Assert( i<n.size() ); @@ -214,10 +276,13 @@ public: return d_children[n[i]].add( n, i+1 ); } } - }; + private: + std::map< Node, NodeTrie > d_children; + }; /* class NodeTrie */ + std::map< int, NodeTrie > d_clique_trie; void addClique( int c, std::vector< Node >& clique ); - private: + /** Are we in conflict */ context::CDO<bool> d_conflict; /** cardinality */ @@ -232,8 +297,6 @@ public: 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 */ @@ -246,18 +309,20 @@ public: context::CDO< bool > d_initialized; /** cache for lemmas */ NodeBoolMap d_lemma_cache; - private: + /** apply totality */ bool applyTotality( int cardinality ); /** get totality lemma terms */ Node getTotalityLemmaTerm( int cardinality, int i ); /** simple check cardinality */ void simpleCheckCardinality(); - private: + bool doSendLemma( Node lem ); + public: - SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ); - virtual ~SortModel(){} + SortModel( Node n, context::Context* c, context::UserContext* u, + StrongSolverTheoryUF* thss ); + virtual ~SortModel(); /** initialize */ void initialize( OutputChannel* out ); /** new node */ @@ -420,18 +485,7 @@ public: Statistics d_statistics; };/* class StrongSolverTheoryUF */ -class DisequalityPropagator -{ -private: - /** quantifiers engine */ - QuantifiersEngine* d_qe; - /** strong solver */ - StrongSolverTheoryUF* d_ufss; - /** true,false */ - Node d_true; - Node d_false; - /** check term t against equivalence class that t is disequal from */ - void checkEquivalenceClass( Node t, Node eqc ); +class DisequalityPropagator { public: DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss); /** merge */ @@ -440,7 +494,7 @@ public: void assertDisequal( Node a, Node b, Node reason ); /** assert predicate */ void assertPredicate( Node p, bool polarity ); -public: + class Statistics { public: IntStat d_propagations; @@ -449,9 +503,20 @@ public: }; /** statistics class */ Statistics d_statistics; -}; -} +private: + /** quantifiers engine */ + QuantifiersEngine* d_qe; + /** strong solver */ + StrongSolverTheoryUF* d_ufss; + /** true,false */ + Node d_true; + Node d_false; + /** check term t against equivalence class that t is disequal from */ + void checkEquivalenceClass( Node t, Node eqc ); +}; /* class DisequalityPropagator */ + +}/* CVC4::theory namespace::uf */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 05b95e9e1..ab42aaf15 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_uf_type_rules.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Christopher L. Conway, Andrew Reynolds, Morgan Deters - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add brief comments here ]] ** |