summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/abstract_values.cpp55
-rw-r--r--src/smt/abstract_values.h80
-rw-r--r--src/smt/smt_engine.cpp76
-rw-r--r--src/smt/smt_engine.h4
4 files changed, 152 insertions, 63 deletions
diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp
new file mode 100644
index 000000000..07c517048
--- /dev/null
+++ b/src/smt/abstract_values.cpp
@@ -0,0 +1,55 @@
+/********************* */
+/*! \file abstract_values.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Utility for constructing and maintaining abstract values.
+ **/
+
+#include "smt/abstract_values.h"
+
+#include "options/smt_options.h"
+
+namespace CVC4 {
+namespace smt {
+
+AbstractValues::AbstractValues(NodeManager* nm)
+ : d_nm(nm),
+ d_fakeContext(),
+ d_abstractValueMap(&d_fakeContext),
+ d_abstractValues()
+{
+}
+AbstractValues::~AbstractValues() {}
+
+Node AbstractValues::substituteAbstractValues(TNode n)
+{
+ // We need to do this even if options::abstractValues() is off,
+ // since the setting might have changed after we already gave out
+ // some abstract values.
+ return d_abstractValueMap.apply(n);
+}
+
+Node AbstractValues::mkAbstractValue(TNode n)
+{
+ Assert(options::abstractValues());
+ Node& val = d_abstractValues[n];
+ if (val.isNull())
+ {
+ val = d_nm->mkAbstractValue(n.getType());
+ d_abstractValueMap.addSubstitution(val, n);
+ }
+ // We are supposed to ascribe types to all abstract values that go out.
+ Node ascription = d_nm->mkConst(AscriptionType(n.getType().toType()));
+ Node retval = d_nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val);
+ return retval;
+}
+
+} // namespace smt
+} // namespace CVC4
diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h
new file mode 100644
index 000000000..9d8f2b439
--- /dev/null
+++ b/src/smt/abstract_values.h
@@ -0,0 +1,80 @@
+/********************* */
+/*! \file abstract_values.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Utility for constructing and maintaining abstract values.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__ABSTRACT_VALUES_H
+#define CVC4__SMT__ABSTRACT_VALUES_H
+
+#include <unordered_map>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/substitutions.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * This utility is responsible for constructing and maintaining abstract
+ * values, which are used in some responses to e.g. get-value / get-model
+ * commands. See SMT-LIB standard 2.6 page 65 for details.
+ */
+class AbstractValues
+{
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+ public:
+ AbstractValues(NodeManager* nm);
+ ~AbstractValues();
+ /**
+ * Substitute away all AbstractValues in a node, which replaces all
+ * abstract values with their original definition. For example, if `@a` was
+ * introduced for term t, then applying this method on f(`@a`) returns f(t).
+ */
+ Node substituteAbstractValues(TNode n);
+
+ /**
+ * Make a new (or return an existing) abstract value for a node.
+ * Can only use this if options::abstractValues() is on.
+ */
+ Node mkAbstractValue(TNode n);
+
+ private:
+ /** Pointer to the used node manager */
+ NodeManager* d_nm;
+ /**
+ * A context that never pushes/pops, for use by CD structures (like
+ * SubstitutionMaps) that should be "global".
+ */
+ context::Context d_fakeContext;
+
+ /**
+ * A map of AbsractValues to their actual constants. Only used if
+ * options::abstractValues() is on.
+ */
+ theory::SubstitutionMap d_abstractValueMap;
+
+ /**
+ * A mapping of all abstract values (actual value |-> abstract) that
+ * we've handed out. This is necessary to ensure that we give the
+ * same AbstractValues for the same real constants. Only used if
+ * options::abstractValues() is on.
+ */
+ NodeToNodeHashMap d_abstractValues;
+};
+
+} // namespace smt
+} // namespace CVC4
+
+#endif
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d80c01035..a3313a733 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -81,6 +81,7 @@
#include "proof/theory_proof.h"
#include "proof/unsat_core.h"
#include "prop/prop_engine.h"
+#include "smt/abstract_values.h"
#include "smt/abduction_solver.h"
#include "smt/command.h"
#include "smt/command_list.h"
@@ -305,29 +306,6 @@ class SmtEnginePrivate : public NodeManagerListener {
// Cached true value
Node d_true;
- /**
- * A context that never pushes/pops, for use by CD structures (like
- * SubstitutionMaps) that should be "global".
- */
- context::Context d_fakeContext;
-
- /**
- * A map of AbsractValues to their actual constants. Only used if
- * options::abstractValues() is on.
- */
- SubstitutionMap d_abstractValueMap;
-
- /**
- * A mapping of all abstract values (actual value |-> abstract) that
- * we've handed out. This is necessary to ensure that we give the
- * same AbstractValues for the same real constants. Only used if
- * options::abstractValues() is on.
- */
- NodeToNodeHashMap d_abstractValues;
-
- /** TODO: whether certain preprocess steps are necessary */
- //bool d_needsExpandDefs;
-
/** The preprocessing pass context */
std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
@@ -375,9 +353,6 @@ class SmtEnginePrivate : public NodeManagerListener {
d_propagator(true, true),
d_assertions(),
d_assertionsProcessed(smt.getUserContext(), false),
- d_fakeContext(),
- d_abstractValueMap(&d_fakeContext),
- d_abstractValues(),
d_processor(smt, *smt.getResourceManager()),
// d_needsExpandDefs(true), //TODO?
d_exprNames(smt.getUserContext()),
@@ -582,34 +557,6 @@ class SmtEnginePrivate : public NodeManagerListener {
return applySubstitutions(n).toExpr();
}
- /**
- * Substitute away all AbstractValues in a node.
- */
- Node substituteAbstractValues(TNode n) {
- // We need to do this even if options::abstractValues() is off,
- // since the setting might have changed after we already gave out
- // some abstract values.
- return d_abstractValueMap.apply(n);
- }
-
- /**
- * Make a new (or return an existing) abstract value for a node.
- * Can only use this if options::abstractValues() is on.
- */
- Node mkAbstractValue(TNode n) {
- Assert(options::abstractValues());
- Node& val = d_abstractValues[n];
- if(val.isNull()) {
- val = d_smt.d_nodeManager->mkAbstractValue(n.getType());
- d_abstractValueMap.addSubstitution(val, n);
- }
- // We are supposed to ascribe types to all abstract values that go out.
- NodeManager* current = d_smt.d_nodeManager;
- Node ascription = current->mkConst(AscriptionType(n.getType().toType()));
- Node retval = current->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val);
- return retval;
- }
-
//------------------------------- expression names
// implements setExpressionName, as described in smt_engine.h
void setExpressionName(Expr e, std::string name) {
@@ -637,6 +584,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
d_userLevels(),
d_exprManager(em),
d_nodeManager(d_exprManager->getNodeManager()),
+ d_absValues(new AbstractValues(d_nodeManager)),
d_theoryEngine(nullptr),
d_propEngine(nullptr),
d_proofManager(nullptr),
@@ -913,6 +861,8 @@ SmtEngine::~SmtEngine()
d_proofManager.reset(nullptr);
#endif
+ d_absValues.reset(nullptr);
+
d_theoryEngine.reset(nullptr);
d_propEngine.reset(nullptr);
@@ -1261,7 +1211,7 @@ void SmtEngine::defineFunction(Expr func,
debugCheckFunctionBody(formula, formals, func);
// Substitute out any abstract values in formula
- Node formNode = d_private->substituteAbstractValues(Node::fromExpr(formula));
+ Node formNode = d_absValues->substituteAbstractValues(Node::fromExpr(formula));
TNode funcNode = func.getTNode();
vector<Node> formalsNodes;
@@ -1367,7 +1317,7 @@ void SmtEngine::defineFunctionsRec(
// assert the quantified formula
// notice we don't call assertFormula directly, since this would
// duplicate the output on raw-benchmark.
- Node n = d_private->substituteAbstractValues(Node::fromExpr(lem));
+ Node n = d_absValues->substituteAbstractValues(Node::fromExpr(lem));
if (d_assertionList != nullptr)
{
d_assertionList->push_back(n);
@@ -1723,7 +1673,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
for (Expr e : d_assumptions)
{
// Substitute out any abstract values in ex.
- Node n = d_private->substituteAbstractValues(Node::fromExpr(e));
+ Node n = d_absValues->substituteAbstractValues(Node::fromExpr(e));
// Ensure expr is type-checked at this point.
ensureBoolean(n);
@@ -1885,7 +1835,7 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
}
// Substitute out any abstract values in ex
- Node n = d_private->substituteAbstractValues(formula);
+ Node n = d_absValues->substituteAbstractValues(formula);
ensureBoolean(n);
if(d_assertionList != NULL) {
@@ -2143,7 +2093,7 @@ Expr SmtEngine::simplify(const Expr& ex)
Dump("benchmark") << SimplifyCommand(ex);
}
- Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
+ Expr e = d_absValues->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
if( options::typeChecking() ) {
e.getType(true); // ensure expr is type-checked at this point
}
@@ -2165,7 +2115,7 @@ Node SmtEngine::expandDefinitions(const Node& ex)
Trace("smt") << "SMT expandDefinitions(" << ex << ")" << endl;
// Substitute out any abstract values in ex.
- Node e = d_private->substituteAbstractValues(ex);
+ Node e = d_absValues->substituteAbstractValues(ex);
if(options::typeChecking()) {
// Ensure expr is type-checked at this point.
e.getType(true);
@@ -2191,7 +2141,7 @@ Expr SmtEngine::getValue(const Expr& ex) const
}
// Substitute out any abstract values in ex.
- Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
+ Expr e = d_absValues->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
// Ensure expr is type-checked at this point.
e.getType(options::typeChecking());
@@ -2242,7 +2192,7 @@ Expr SmtEngine::getValue(const Expr& ex) const
|| resultNode.isConst());
if(options::abstractValues() && resultNode.getType().isArray()) {
- resultNode = d_private->mkAbstractValue(resultNode);
+ resultNode = d_absValues->mkAbstractValue(resultNode);
Trace("smt") << "--- abstract value >> " << resultNode << endl;
}
@@ -2264,7 +2214,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) {
finalOptionsAreSet();
doPendingPops();
// Substitute out any abstract values in ex
- Node n = d_private->substituteAbstractValues(Node::fromExpr(ex));
+ Node n = d_absValues->substituteAbstractValues(Node::fromExpr(ex));
TypeNode type = n.getType(options::typeChecking());
// must be Boolean
PrettyCheckArgument(type.isBoolean(),
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 738a6c22a..591b69424 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -91,6 +91,8 @@ namespace prop {
/* -------------------------------------------------------------------------- */
namespace smt {
+/** Utilities */
+class AbstractValues;
/** Subsolvers */
class AbductionSolver;
/**
@@ -1125,6 +1127,8 @@ class CVC4_PUBLIC SmtEngine
ExprManager* d_exprManager;
/** Our internal expression/node manager */
NodeManager* d_nodeManager;
+ /** Abstract values */
+ std::unique_ptr<smt::AbstractValues> d_absValues;
/** The theory engine */
std::unique_ptr<TheoryEngine> d_theoryEngine;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback