summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/justification_heuristic.cpp86
-rw-r--r--src/decision/justification_heuristic.h28
-rw-r--r--src/theory/theory.cpp5
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/uf/issue4446.smt27
5 files changed, 80 insertions, 47 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index ce79d6ca0..a3873c6da 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -40,10 +40,10 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
d_giveup("decision::jh::giveup", 0),
d_timestat("decision::jh::time"),
d_assertions(uc),
- d_iteAssertions(uc),
- d_iteCache(uc),
+ d_skolemAssertions(uc),
+ d_skolemCache(uc),
d_visited(),
- d_visitedComputeITE(),
+ d_visitedComputeSkolems(),
d_curDecision(),
d_curThreshold(0),
d_childCache(uc),
@@ -175,10 +175,26 @@ void JustificationHeuristic::addAssertions(
<< " assertionsEnd = " << assertionsEnd
<< std::endl;
- // Save the 'real' assertions locally
- for (size_t i = 0; i < assertionsEnd; i++)
+ // Save all assertions locally, including the assertions generated by term
+ // removal. We have to make sure that we assign a value to all the Boolean
+ // term variables. To illustrate why this is, consider the case where we have
+ // a single assertion
+ //
+ // (or (f a) (f b))
+ //
+ // where `f` is a function `Bool -> Bool`. Given an assignment:
+ //
+ // (f a) -> true
+ // (f b) -> false
+ // a -> false
+ //
+ // UF will not complain and the justification heuristic considers the
+ // assertion to be satisifed. However, we also have to make sure that we pick
+ // a value for `b` that is not in conflict with the other assignments (we can
+ // only choose `b` to be `true` otherwise the model is incorrect).
+ for (const Node& assertion : assertions)
{
- d_assertions.push_back(assertions[i]);
+ d_assertions.push_back(assertion);
}
// Save mapping between ite skolems and ite assertions
@@ -188,7 +204,7 @@ void JustificationHeuristic::addAssertions(
<< assertions[(i.second)] << std::endl;
Assert(i.second >= assertionsEnd && i.second < assertions.size());
- d_iteAssertions[i.first] = assertions[i.second];
+ d_skolemAssertions[i.first] = assertions[i.second];
}
// Automatic weight computation
@@ -363,36 +379,39 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
}//end of else
}
-JustificationHeuristic::IteList
-JustificationHeuristic::getITEs(TNode n)
+JustificationHeuristic::SkolemList JustificationHeuristic::getSkolems(TNode n)
{
- IteCache::iterator it = d_iteCache.find(n);
- if(it != d_iteCache.end()) {
+ SkolemCache::iterator it = d_skolemCache.find(n);
+ if (it != d_skolemCache.end())
+ {
return (*it).second;
- } else {
- // Compute the list of ITEs
- // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
- d_visitedComputeITE.clear();
- IteList ilist;
- computeITEs(n, ilist);
- d_iteCache.insert(n, ilist);
+ }
+ else
+ {
+ // Compute the list of Skolems
+ // TODO: optimize by avoiding multiple lookup for d_skolemCache[n]
+ d_visitedComputeSkolems.clear();
+ SkolemList ilist;
+ computeSkolems(n, ilist);
+ d_skolemCache.insert(n, ilist);
return ilist;
}
}
-void JustificationHeuristic::computeITEs(TNode n, IteList &l)
+void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l)
{
- Trace("decision::jh::ite") << " computeITEs( " << n << ", &l)\n";
- d_visitedComputeITE.insert(n);
+ Trace("decision::jh::skolems") << " computeSkolems( " << n << ", &l)\n";
+ d_visitedComputeSkolems.insert(n);
for(unsigned i=0; i<n.getNumChildren(); ++i) {
- SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
- if(it2 != d_iteAssertions.end()) {
+ SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]);
+ if (it2 != d_skolemAssertions.end())
+ {
l.push_back(make_pair(n[i], (*it2).second));
Assert(n[i].getNumChildren() == 0);
}
- if(d_visitedComputeITE.find(n[i]) ==
- d_visitedComputeITE.end()) {
- computeITEs(n[i], l);
+ if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end())
+ {
+ computeSkolems(n[i], l);
}
}
}
@@ -470,9 +489,8 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
* If not in theory of booleans, check if this is something to split-on.
*/
if(isAtom) {
- // if node has embedded ites, resolve that first
- if(handleEmbeddedITEs(node) == FOUND_SPLITTER)
- return FOUND_SPLITTER;
+ // if node has embedded skolems due to term removal, resolve that first
+ if (handleEmbeddedSkolems(node) == FOUND_SPLITTER) return FOUND_SPLITTER;
if(litVal != SAT_VALUE_UNKNOWN) {
Assert(litVal == desiredVal);
@@ -700,13 +718,15 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode nod
}// else (...ifVal...)
}
-JustificationHeuristic::SearchResult JustificationHeuristic::handleEmbeddedITEs(TNode node)
+JustificationHeuristic::SearchResult
+JustificationHeuristic::handleEmbeddedSkolems(TNode node)
{
- const IteList l = getITEs(node);
- Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl;
+ const SkolemList l = getSkolems(node);
+ Trace("decision::jh::skolems") << " skolems size = " << l.size() << std::endl;
bool noSplitter = true;
- for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
+ for (SkolemList::const_iterator i = l.begin(); i != l.end(); ++i)
+ {
if(d_visited.find((*i).first) == d_visited.end()) {
d_visited.insert((*i).first);
SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE);
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index bb426ad1e..9e6765438 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -42,8 +42,8 @@ class JustificationHeuristic : public ITEDecisionStrategy {
// TRUE FALSE MEH
enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
- typedef std::vector<pair<TNode,TNode> > IteList;
- typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache;
+ typedef std::vector<pair<TNode, TNode> > SkolemList;
+ typedef context::CDHashMap<TNode, SkolemList, TNodeHashFunction> SkolemCache;
typedef std::vector<TNode> ChildList;
typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache;
typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
@@ -63,18 +63,19 @@ class JustificationHeuristic : public ITEDecisionStrategy {
/**
* A copy of the assertions that need to be justified
- * directly. Doesn't have ones introduced during during ITE-removal.
+ * directly. Doesn't have ones introduced during during term removal.
*/
context::CDList<TNode> d_assertions;
//TNode is fine since decisionEngine has them too
- /** map from ite-rewrite skolem to a boolean-ite assertion */
- SkolemMap d_iteAssertions;
+ /** map from skolems introduced in term removal to the corresponding assertion
+ */
+ SkolemMap d_skolemAssertions;
// 'key' being TNode is fine since if a skolem didn't exist anywhere,
// we won't look it up. as for 'value', same reason as d_assertions
- /** Cache for ITE skolems present in a atomic formula */
- IteCache d_iteCache;
+ /** Cache for skolems present in a atomic formula */
+ SkolemCache d_skolemCache;
/**
* This is used to prevent infinite loop when trying to find a
@@ -84,10 +85,10 @@ class JustificationHeuristic : public ITEDecisionStrategy {
std::unordered_set<TNode,TNodeHashFunction> d_visited;
/**
- * Set to track visited nodes in a dfs search done in computeITE
+ * Set to track visited nodes in a dfs search done in computeSkolems
* function
*/
- std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE;
+ std::unordered_set<TNode, TNodeHashFunction> d_visitedComputeSkolems;
/** current decision for the recursive call */
SatLiteral d_curDecision;
@@ -153,8 +154,7 @@ public:
SatValue tryGetSatValue(Node n);
/* Get list of all term-ITEs for the atomic formula v */
- JustificationHeuristic::IteList getITEs(TNode n);
-
+ JustificationHeuristic::SkolemList getSkolems(TNode n);
/**
* For big and/or nodes, a cache to save starting index into children
@@ -165,8 +165,8 @@ public:
int getStartIndex(TNode node);
void saveStartIndex(TNode node, int val);
- /* Compute all term-ITEs in a node recursively */
- void computeITEs(TNode n, IteList &l);
+ /* Compute all term-removal skolems in a node recursively */
+ void computeSkolems(TNode n, SkolemList& l);
SearchResult handleAndOrEasy(TNode node, SatValue desiredVal);
SearchResult handleAndOrHard(TNode node, SatValue desiredVal);
@@ -175,7 +175,7 @@ public:
SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1,
TNode node2, SatValue desiredVal2);
SearchResult handleITE(TNode node, SatValue desiredVal);
- SearchResult handleEmbeddedITEs(TNode node);
+ SearchResult handleEmbeddedSkolems(TNode node);
};/* class JustificationHeuristic */
}/* namespace decision */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 3069461fa..efe01dda4 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -271,6 +271,11 @@ void Theory::debugPrintFacts() const{
bool Theory::isLegalElimination(TNode x, TNode val)
{
Assert(x.isVar());
+ if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
+ || val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+ {
+ return false;
+ }
if (expr::hasSubterm(val, x))
{
return false;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 290fca6bc..f6bc70cd0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1089,6 +1089,7 @@ set(regress_0_tests
regress0/uf/euf_simp13.smtv1.smt2
regress0/uf/iso_brn001.smtv1.smt2
regress0/uf/issue2947.smt2
+ regress0/uf/issue4446.smt2
regress0/uf/pred.smtv1.smt2
regress0/uf/simple.01.cvc
regress0/uf/simple.02.cvc
diff --git a/test/regress/regress0/uf/issue4446.smt2 b/test/regress/regress0/uf/issue4446.smt2
new file mode 100644
index 000000000..e59c3ee10
--- /dev/null
+++ b/test/regress/regress0/uf/issue4446.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_AUFLIA)
+(declare-fun a (Bool) Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (or (a b) (a c)))
+(set-info :status sat)
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback