From 144c4df45ecedff8bfdbf8672e376606b393fc84 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 16 Jul 2020 14:00:59 -0500 Subject: Split abstract values utility from SmtEngine (#4754) Towards refactoring SmtEngine. --- src/CMakeLists.txt | 2 ++ src/smt/abstract_values.cpp | 55 +++++++++++++++++++++++++++++++ src/smt/abstract_values.h | 80 +++++++++++++++++++++++++++++++++++++++++++++ src/smt/smt_engine.cpp | 76 ++++++++---------------------------------- src/smt/smt_engine.h | 4 +++ 5 files changed, 154 insertions(+), 63 deletions(-) create mode 100644 src/smt/abstract_values.cpp create mode 100644 src/smt/abstract_values.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a19580c00..4f87778a3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -221,6 +221,8 @@ libcvc4_add_sources( prop/theory_proxy.h smt/abduction_solver.cpp smt/abduction_solver.h + smt/abstract_values.cpp + smt/abstract_values.h smt/command.cpp smt/command.h smt/command_list.cpp 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 + +#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 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 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 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& 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 d_absValues; /** The theory engine */ std::unique_ptr d_theoryEngine; -- cgit v1.2.3