--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
#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"
// 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;
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()),
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) {
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),
d_proofManager.reset(nullptr);
#endif
+ d_absValues.reset(nullptr);
+
d_theoryEngine.reset(nullptr);
d_propEngine.reset(nullptr);
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;
// 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);
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);
}
// 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) {
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
}
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);
}
// 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());
|| resultNode.isConst());
if(options::abstractValues() && resultNode.getType().isArray()) {
- resultNode = d_private->mkAbstractValue(resultNode);
+ resultNode = d_absValues->mkAbstractValue(resultNode);
Trace("smt") << "--- abstract value >> " << resultNode << endl;
}
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(),
projects / cvc5.git / commitdiff