summaryrefslogtreecommitdiff
path: root/src/smt/model_blocker.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/model_blocker.cpp')
-rw-r--r--src/smt/model_blocker.cpp288
1 files changed, 288 insertions, 0 deletions
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
new file mode 100644
index 000000000..cb962ee45
--- /dev/null
+++ b/src/smt/model_blocker.cpp
@@ -0,0 +1,288 @@
+/********************* */
+/*! \file model_blocker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of utility for blocking models.
+ **
+ **/
+
+#include "smt/model_blocker.h"
+
+#include "expr/node.h"
+#include "expr/node_algorithm.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
+ theory::TheoryModel* m,
+ BlockModelsMode mode,
+ const std::vector<Expr>& exprToBlock)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ // convert to nodes
+ std::vector<Node> tlAsserts;
+ for (const Expr& a : assertions)
+ {
+ Node an = Node::fromExpr(a);
+ tlAsserts.push_back(an);
+ }
+ std::vector<Node> nodesToBlock;
+ for (const Expr& eb : exprToBlock)
+ {
+ nodesToBlock.push_back(Node::fromExpr(eb));
+ }
+ Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
+ Node blocker;
+ if (mode == BLOCK_MODELS_LITERALS)
+ {
+ Assert(nodesToBlock.empty());
+ // optimization: filter out top-level unit assertions, as they cannot
+ // contribute to model blocking.
+ unsigned counter = 0;
+ std::vector<Node> asserts;
+ while (counter < tlAsserts.size())
+ {
+ Node cur = tlAsserts[counter];
+ counter++;
+ Node catom = cur.getKind() == NOT ? cur[0] : cur;
+ bool cpol = cur.getKind() != NOT;
+ if (catom.getKind() == NOT)
+ {
+ tlAsserts.push_back(catom[0]);
+ }
+ else if (catom.getKind() == AND && cpol)
+ {
+ tlAsserts.insert(tlAsserts.end(), catom.begin(), catom.end());
+ }
+ else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
+ {
+ asserts.push_back(cur);
+ Trace("model-blocker") << " " << cur << std::endl;
+ }
+ }
+ if (asserts.empty())
+ {
+ Node blockTriv = nm->mkConst(false);
+ Trace("model-blocker")
+ << "...model blocker is (trivially) " << blockTriv << std::endl;
+ return blockTriv.toExpr();
+ }
+
+ Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0];
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction> implicant;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(formula);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ Trace("model-blocker-debug") << "Visit : " << cur << std::endl;
+
+ if (it == visited.end())
+ {
+ visited[cur] = Node::null();
+ Node catom = cur.getKind() == NOT ? cur[0] : cur;
+ bool cpol = cur.getKind() != NOT;
+ // compute the implicant
+ // impl is a formula that implies cur that is also satisfied by m
+ Node impl;
+ if (catom.getKind() == NOT)
+ {
+ // double negation
+ impl = catom[0];
+ }
+ else if (catom.getKind() == OR || catom.getKind() == AND)
+ {
+ // if disjunctive
+ if ((catom.getKind() == OR) == cpol)
+ {
+ // take the first literal that is satisfied
+ for (Node n : catom)
+ {
+ // rewrite, this ensures that e.g. the propositional value of
+ // quantified formulas can be queried
+ n = theory::Rewriter::rewrite(n);
+ Node vn = Node::fromExpr(m->getValue(n.toExpr()));
+ Assert(vn.isConst());
+ if (vn.getConst<bool>() == cpol)
+ {
+ impl = cpol ? n : n.negate();
+ break;
+ }
+ }
+ }
+ else if (catom.getKind() == OR)
+ {
+ // one step NNF
+ std::vector<Node> children;
+ for (const Node& cn : catom)
+ {
+ children.push_back(cn.negate());
+ }
+ impl = nm->mkNode(AND, children);
+ }
+ }
+ else if (catom.getKind() == ITE)
+ {
+ Node vcond = Node::fromExpr(m->getValue(cur[0].toExpr()));
+ Assert(vcond.isConst());
+ Node cond = cur[0];
+ Node branch;
+ if (vcond.getConst<bool>())
+ {
+ branch = cur[1];
+ }
+ else
+ {
+ cond = cond.negate();
+ branch = cur[2];
+ }
+ impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate());
+ }
+ else if ((catom.getKind() == EQUAL && catom[0].getType().isBoolean())
+ || catom.getKind() == XOR)
+ {
+ // based on how the children evaluate in the model
+ std::vector<Node> children;
+ for (const Node& cn : catom)
+ {
+ Node vn = Node::fromExpr(m->getValue(cn.toExpr()));
+ Assert(vn.isConst());
+ children.push_back(vn.getConst<bool>() ? cn : cn.negate());
+ }
+ impl = nm->mkNode(AND, children);
+ }
+ else
+ {
+ // literals justified by themselves
+ visited[cur] = cur;
+ Trace("model-blocker-debug") << "...self justified" << std::endl;
+ }
+ if (visited[cur].isNull())
+ {
+ visit.push_back(cur);
+ if (impl.isNull())
+ {
+ Assert(cur.getKind() == AND);
+ Trace("model-blocker-debug") << "...recurse" << std::endl;
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ else
+ {
+ Trace("model-blocker-debug")
+ << "...implicant : " << impl << std::endl;
+ implicant[cur] = impl;
+ visit.push_back(impl);
+ }
+ }
+ }
+ else if (it->second.isNull())
+ {
+ Node ret = cur;
+ it = implicant.find(cur);
+ if (it != implicant.end())
+ {
+ Node impl = it->second;
+ it = visited.find(impl);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ ret = it->second;
+ Trace("model-blocker-debug")
+ << "...implicant res: " << ret << std::endl;
+ }
+ else
+ {
+ bool childChanged = false;
+ std::vector<Node> children;
+ // we never recurse to parameterized nodes
+ Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
+ for (const Node& cn : cur)
+ {
+ it = visited.find(cn);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ childChanged = childChanged || cn != it->second;
+ children.push_back(it->second);
+ }
+ if (childChanged)
+ {
+ ret = nm->mkNode(cur.getKind(), children);
+ }
+ Trace("model-blocker-debug") << "...recons res: " << ret << std::endl;
+ }
+ visited[cur] = ret;
+ }
+ } while (!visit.empty());
+ Assert(visited.find(formula) != visited.end());
+ Assert(!visited.find(formula)->second.isNull());
+ blocker = visited[formula].negate();
+ }
+ else
+ {
+ Assert(mode == BLOCK_MODELS_VALUES);
+ std::vector<Node> blockers;
+ // if specific terms were not specified, block all variables of
+ // the model
+ if (nodesToBlock.empty())
+ {
+ Trace("model-blocker")
+ << "no specific terms to block recognized" << std::endl;
+ std::unordered_set<Node, NodeHashFunction> symbols;
+ for (Node n : tlAsserts)
+ {
+ expr::getSymbols(n, symbols);
+ }
+ for (Node s : symbols)
+ {
+ if (s.getType().getKind() != kind::FUNCTION_TYPE)
+ {
+ Node v = m->getValue(s);
+ Node a = nm->mkNode(DISTINCT, s, v);
+ blockers.push_back(a);
+ }
+ }
+ }
+ // otherwise, block all terms that were specified in get-value
+ else
+ {
+ std::unordered_set<Node, NodeHashFunction> terms;
+ for (Node n : nodesToBlock)
+ {
+ Node v = m->getValue(n);
+ Node a = nm->mkNode(DISTINCT, n, v);
+ blockers.push_back(a);
+ }
+ }
+ if (blockers.size() == 0)
+ {
+ blocker = nm->mkConst<bool>(true);
+ }
+ else if (blockers.size() == 1)
+ {
+ blocker = blockers[0];
+ }
+ else
+ {
+ blocker = nm->mkNode(OR, blockers);
+ }
+ }
+ Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
+ return blocker.toExpr();
+}
+
+} /* namespace CVC4 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback