This is a step towards refactoring the SmtEngine. It splits several core components of SmtEnginePrivate to its own independent module, ProcessAssertions which is responsible for applying preprocessing passes , simplification and expand definitions.
The main change involved moving these functions from SmtEnginePrivate to this new class. A few other minor changes were done to make this move:
A few things changed order within processAssertions to allow SmtEnginePrivate-specific things to happen outside of the main scope of processAssertions.
processAssertions had some logic to catch incompatible options and silently disable options. This was moved to setDefaults.
A few data members in SmtEngine were moved to ProcessAssertions.
Two utilities that were sitting in smt_engine.cpp were moved to their own files.
Another refactoring step will be to make ProcessAssertions take only the utilities it needs instead of taking a SmtEngine reference. This requires further detangling of Options.
smt/command.h
smt/command_list.cpp
smt/command_list.h
+ smt/defined_function.h
smt/dump.cpp
smt/dump.h
smt/logic_exception.h
smt/model_core_builder.h
smt/model_blocker.cpp
smt/model_blocker.h
+ smt/process_assertions.cpp
+ smt/process_assertions.h
smt/set_defaults.cpp
smt/set_defaults.h
smt/smt_engine.cpp
smt/smt_engine.h
smt/smt_engine_scope.cpp
smt/smt_engine_scope.h
+ smt/smt_engine_stats.cpp
+ smt/smt_engine_stats.h
smt/smt_statistics_registry.cpp
smt/smt_statistics_registry.h
smt/term_formula_removal.cpp
long = "miplib-trick"
type = "bool"
default = "false"
- read_only = true
help = "turns on the preprocessing step of attempting to infer bounds on miplib problems"
[[option]]
--- /dev/null
+/********************* */
+/*! \file defined_function.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 Defined function data structure
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__DEFINED_FUNCTION_H
+#define CVC4__SMT__DEFINED_FUNCTION_H
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * Representation of a defined function. We keep these around in
+ * SmtEngine to permit expanding definitions late (and lazily), to
+ * support getValue() over defined functions, to support user output
+ * in terms of defined functions, etc.
+ */
+class DefinedFunction
+{
+ public:
+ DefinedFunction() {}
+ DefinedFunction(Node func, std::vector<Node>& formals, Node formula)
+ : d_func(func), d_formals(formals), d_formula(formula)
+ {
+ }
+ /** get the function */
+ Node getFunction() const { return d_func; }
+ /** get the formal argument list of the function */
+ const std::vector<Node>& getFormals() const { return d_formals; }
+ /** get the formula that defines it */
+ Node getFormula() const { return d_formula; }
+
+ private:
+ /** the function */
+ Node d_func;
+ /** the formal argument list */
+ std::vector<Node> d_formals;
+ /** the formula */
+ Node d_formula;
+}; /* class DefinedFunction */
+
+} // namespace smt
+} // namespace CVC4
+
+#endif /* CVC4__SMT__DEFINED_FUNCTION_H */
--- /dev/null
+/********************* */
+/*! \file process_assertions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andrew Reynolds, Tim King
+ ** 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 module for processing assertions for an SMT engine.
+ **/
+
+#include "smt/process_assertions.h"
+
+#include <stack>
+#include <utility>
+
+#include "expr/node_manager_attributes.h"
+#include "options/arith_options.h"
+#include "options/base_options.h"
+#include "options/bv_options.h"
+#include "options/proof_options.h"
+#include "options/quantifiers_options.h"
+#include "options/sep_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_registry.h"
+#include "smt/defined_function.h"
+#include "smt/smt_engine.h"
+#include "theory/logic_info.h"
+#include "theory/quantifiers/fun_def_process.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::preprocessing;
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace smt {
+
+/** Useful for counting the number of recursive calls. */
+class ScopeCounter
+{
+ public:
+ ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
+ ~ScopeCounter() { --d_depth; }
+
+ private:
+ unsigned& d_depth;
+};
+
+ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm)
+ : d_smt(smt),
+ d_resourceManager(rm),
+ d_preprocessingPassContext(nullptr),
+ d_fmfRecFunctionsDefined(nullptr)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_fmfRecFunctionsDefined = new (true) NodeList(d_smt.getUserContext());
+}
+
+ProcessAssertions::~ProcessAssertions()
+{
+ d_fmfRecFunctionsDefined->deleteSelf();
+}
+
+void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
+{
+ Assert(d_preprocessingPassContext == nullptr);
+ d_preprocessingPassContext = pc;
+
+ PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
+ // TODO: this will likely change when we add support for actually assembling
+ // preprocessing pipelines. For now, we just create an instance of each
+ // available preprocessing pass.
+ std::vector<std::string> passNames = ppReg.getAvailablePasses();
+ for (const std::string& passName : passNames)
+ {
+ d_passes[passName].reset(
+ ppReg.createPass(d_preprocessingPassContext, passName));
+ }
+}
+
+void ProcessAssertions::cleanup() { d_passes.clear(); }
+
+void ProcessAssertions::spendResource(ResourceManager::Resource r)
+{
+ d_resourceManager.spendResource(r);
+}
+
+bool ProcessAssertions::apply(AssertionPipeline& assertions)
+{
+ Assert(d_preprocessingPassContext != nullptr);
+ // Dump the assertions
+ dumpAssertions("pre-everything", assertions);
+
+ Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
+ Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
+
+ Debug("smt") << "#Assertions : " << assertions.size() << endl;
+ Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;
+
+ if (assertions.size() == 0)
+ {
+ // nothing to do
+ return true;
+ }
+
+ SubstitutionMap& top_level_substs =
+ d_preprocessingPassContext->getTopLevelSubstitutions();
+
+ if (options::bvGaussElim())
+ {
+ d_passes["bv-gauss"]->apply(&assertions);
+ }
+
+ // Add dummy assertion in last position - to be used as a
+ // placeholder for any new assertions to get added
+ assertions.push_back(d_true);
+ // any assertions added beyond realAssertionsEnd must NOT affect the
+ // equisatisfiability
+ assertions.updateRealAssertionsEnd();
+
+ // Assertions are NOT guaranteed to be rewritten by this point
+
+ Trace("smt-proc")
+ << "ProcessAssertions::processAssertions() : pre-definition-expansion"
+ << endl;
+ dumpAssertions("pre-definition-expansion", assertions);
+ {
+ Chat() << "expanding definitions..." << endl;
+ Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions"
+ << endl;
+ TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
+ unordered_map<Node, Node, NodeHashFunction> cache;
+ for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
+ {
+ assertions.replace(i, expandDefinitions(assertions[i], cache));
+ }
+ }
+ Trace("smt-proc")
+ << "ProcessAssertions::processAssertions() : post-definition-expansion"
+ << endl;
+ dumpAssertions("post-definition-expansion", assertions);
+
+ // save the assertions now
+ THEORY_PROOF(
+ for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) {
+ ProofManager::currentPM()->addAssertion(assertions[i].toExpr());
+ });
+
+ Debug("smt") << " assertions : " << assertions.size() << endl;
+
+ if (options::globalNegate())
+ {
+ // global negation of the formula
+ d_passes["global-negate"]->apply(&assertions);
+ d_smt.d_globalNegation = !d_smt.d_globalNegation;
+ }
+
+ if (options::nlExtPurify())
+ {
+ d_passes["nl-ext-purify"]->apply(&assertions);
+ }
+
+ if (options::solveRealAsInt())
+ {
+ d_passes["real-to-int"]->apply(&assertions);
+ }
+
+ if (options::solveIntAsBV() > 0)
+ {
+ d_passes["int-to-bv"]->apply(&assertions);
+ }
+
+ if (options::ackermann())
+ {
+ d_passes["ackermann"]->apply(&assertions);
+ }
+
+ if (options::bvAbstraction())
+ {
+ d_passes["bv-abstraction"]->apply(&assertions);
+ }
+
+ Debug("smt") << " assertions : " << assertions.size() << endl;
+
+ bool noConflict = true;
+
+ if (options::extRewPrep())
+ {
+ d_passes["ext-rew-pre"]->apply(&assertions);
+ }
+
+ // Unconstrained simplification
+ if (options::unconstrainedSimp())
+ {
+ d_passes["rewrite"]->apply(&assertions);
+ d_passes["unconstrained-simplifier"]->apply(&assertions);
+ }
+
+ if (options::bvIntroducePow2())
+ {
+ d_passes["bv-intro-pow2"]->apply(&assertions);
+ }
+
+ // Since this pass is not robust for the information tracking necessary for
+ // unsat cores, it's only applied if we are not doing unsat core computation
+ if (!options::unsatCores())
+ {
+ d_passes["apply-substs"]->apply(&assertions);
+ }
+
+ // Assertions MUST BE guaranteed to be rewritten by this point
+ d_passes["rewrite"]->apply(&assertions);
+
+ // Lift bit-vectors of size 1 to bool
+ if (options::bitvectorToBool())
+ {
+ d_passes["bv-to-bool"]->apply(&assertions);
+ }
+ if (options::solveBVAsInt() > 0)
+ {
+ d_passes["bv-to-int"]->apply(&assertions);
+ }
+
+ // Convert non-top-level Booleans to bit-vectors of size 1
+ if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+ {
+ d_passes["bool-to-bv"]->apply(&assertions);
+ }
+ if (options::sepPreSkolemEmp())
+ {
+ d_passes["sep-skolem-emp"]->apply(&assertions);
+ }
+
+ if (d_smt.d_logic.isQuantified())
+ {
+ // remove rewrite rules, apply pre-skolemization to existential quantifiers
+ d_passes["quantifiers-preprocess"]->apply(&assertions);
+ if (options::macrosQuant())
+ {
+ // quantifiers macro expansion
+ d_passes["quantifier-macros"]->apply(&assertions);
+ }
+
+ // fmf-fun : assume admissible functions, applying preprocessing reduction
+ // to FMF
+ if (options::fmfFunWellDefined())
+ {
+ quantifiers::FunDefFmf fdf;
+ Assert(d_fmfRecFunctionsDefined != NULL);
+ // must carry over current definitions (in case of incremental)
+ for (context::CDList<Node>::const_iterator fit =
+ d_fmfRecFunctionsDefined->begin();
+ fit != d_fmfRecFunctionsDefined->end();
+ ++fit)
+ {
+ Node f = (*fit);
+ Assert(d_fmfRecFunctionsAbs.find(f) != d_fmfRecFunctionsAbs.end());
+ TypeNode ft = d_fmfRecFunctionsAbs[f];
+ fdf.d_sorts[f] = ft;
+ std::map<Node, std::vector<Node>>::iterator fcit =
+ d_fmfRecFunctionsConcrete.find(f);
+ Assert(fcit != d_fmfRecFunctionsConcrete.end());
+ for (const Node& fcc : fcit->second)
+ {
+ fdf.d_input_arg_inj[f].push_back(fcc);
+ }
+ }
+ fdf.simplify(assertions.ref());
+ // must store new definitions (in case of incremental)
+ for (const Node& f : fdf.d_funcs)
+ {
+ d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
+ d_fmfRecFunctionsConcrete[f].clear();
+ for (const Node& fcc : fdf.d_input_arg_inj[f])
+ {
+ d_fmfRecFunctionsConcrete[f].push_back(fcc);
+ }
+ d_fmfRecFunctionsDefined->push_back(f);
+ }
+ }
+ }
+
+ if (options::sortInference() || options::ufssFairnessMonotone())
+ {
+ d_passes["sort-inference"]->apply(&assertions);
+ }
+
+ if (options::pbRewrites())
+ {
+ d_passes["pseudo-boolean-processor"]->apply(&assertions);
+ }
+
+ // rephrasing normal inputs as sygus problems
+ if (!d_smt.d_isInternalSubsolver)
+ {
+ if (options::sygusInference())
+ {
+ d_passes["sygus-infer"]->apply(&assertions);
+ }
+ else if (options::sygusRewSynthInput())
+ {
+ // do candidate rewrite rule synthesis
+ d_passes["synth-rr"]->apply(&assertions);
+ }
+ }
+
+ Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
+ << endl;
+ dumpAssertions("pre-simplify", assertions);
+ Chat() << "simplifying assertions..." << endl;
+ noConflict = simplifyAssertions(assertions);
+ if (!noConflict)
+ {
+ ++(d_smt.d_stats->d_simplifiedToFalse);
+ }
+ Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
+ << endl;
+ dumpAssertions("post-simplify", assertions);
+
+ if (options::doStaticLearning())
+ {
+ d_passes["static-learning"]->apply(&assertions);
+ }
+ Debug("smt") << " assertions : " << assertions.size() << endl;
+
+ {
+ d_smt.d_stats->d_numAssertionsPre += assertions.size();
+ d_passes["ite-removal"]->apply(&assertions);
+ // This is needed because when solving incrementally, removeITEs may
+ // introduce skolems that were solved for earlier and thus appear in the
+ // substitution map.
+ d_passes["apply-substs"]->apply(&assertions);
+ d_smt.d_stats->d_numAssertionsPost += assertions.size();
+ }
+
+ dumpAssertions("pre-repeat-simplify", assertions);
+ if (options::repeatSimp())
+ {
+ Trace("smt-proc")
+ << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
+ << endl;
+ Chat() << "re-simplifying assertions..." << endl;
+ ScopeCounter depth(d_simplifyAssertionsDepth);
+ noConflict &= simplifyAssertions(assertions);
+ if (noConflict)
+ {
+ // Need to fix up assertion list to maintain invariants:
+ // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be
+ // the order in which these variables were introduced during ite removal.
+ // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr
+ // mapped to by sk.
+
+ // cache for expression traversal
+ unordered_map<Node, bool, NodeHashFunction> cache;
+
+ IteSkolemMap& iskMap = assertions.getIteSkolemMap();
+ // First, find all skolems that appear in the substitution map - their
+ // associated iteExpr will need to be moved to the main assertion set
+ set<TNode> skolemSet;
+ SubstitutionMap::iterator pos = top_level_substs.begin();
+ for (; pos != top_level_substs.end(); ++pos)
+ {
+ collectSkolems(iskMap, (*pos).first, skolemSet, cache);
+ collectSkolems(iskMap, (*pos).second, skolemSet, cache);
+ }
+ // We need to ensure:
+ // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
+ // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
+ // If either of these is violated, we must add iteExpr as a proper
+ // assertion
+ IteSkolemMap::iterator it = iskMap.begin();
+ IteSkolemMap::iterator iend = iskMap.end();
+ NodeBuilder<> builder(AND);
+ builder << assertions[assertions.getRealAssertionsEnd() - 1];
+ vector<TNode> toErase;
+ for (; it != iend; ++it)
+ {
+ if (skolemSet.find((*it).first) == skolemSet.end())
+ {
+ TNode iteExpr = assertions[(*it).second];
+ if (iteExpr.getKind() == ITE && iteExpr[1].getKind() == EQUAL
+ && iteExpr[1][0] == (*it).first && iteExpr[2].getKind() == EQUAL
+ && iteExpr[2][0] == (*it).first)
+ {
+ cache.clear();
+ bool bad =
+ checkForBadSkolems(iskMap, iteExpr[0], (*it).first, cache);
+ bad = bad
+ || checkForBadSkolems(
+ iskMap, iteExpr[1][1], (*it).first, cache);
+ bad = bad
+ || checkForBadSkolems(
+ iskMap, iteExpr[2][1], (*it).first, cache);
+ if (!bad)
+ {
+ continue;
+ }
+ }
+ }
+ // Move this iteExpr into the main assertions
+ builder << assertions[(*it).second];
+ assertions[(*it).second] = d_true;
+ toErase.push_back((*it).first);
+ }
+ if (builder.getNumChildren() > 1)
+ {
+ while (!toErase.empty())
+ {
+ iskMap.erase(toErase.back());
+ toErase.pop_back();
+ }
+ assertions[assertions.getRealAssertionsEnd() - 1] =
+ Rewriter::rewrite(Node(builder));
+ }
+ // TODO(b/1256): For some reason this is needed for some benchmarks, such
+ // as
+ // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
+ d_passes["ite-removal"]->apply(&assertions);
+ d_passes["apply-substs"]->apply(&assertions);
+ }
+ Trace("smt-proc")
+ << "ProcessAssertions::processAssertions() : post-repeat-simplify"
+ << endl;
+ }
+ dumpAssertions("post-repeat-simplify", assertions);
+
+ if (options::ufHo())
+ {
+ d_passes["ho-elim"]->apply(&assertions);
+ }
+
+ // begin: INVARIANT to maintain: no reordering of assertions or
+ // introducing new ones
+
+ Debug("smt") << " assertions : " << assertions.size() << endl;
+
+ Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
+ << endl;
+ Debug("smt") << " assertions : " << assertions.size() << endl;
+
+ d_passes["theory-preprocess"]->apply(&assertions);
+
+ if (options::bitblastMode() == options::BitblastMode::EAGER)
+ {
+ d_passes["bv-eager-atoms"]->apply(&assertions);
+ }
+
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
+ dumpAssertions("post-everything", assertions);
+
+ return noConflict;
+}
+
+// returns false if simplification led to "false"
+bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
+{
+ spendResource(ResourceManager::Resource::PreprocessStep);
+ Assert(d_smt.d_pendingPops == 0);
+ try
+ {
+ ScopeCounter depth(d_simplifyAssertionsDepth);
+
+ Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
+
+ if (options::simplificationMode() != options::SimplificationMode::NONE)
+ {
+ if (!options::unsatCores() && !options::fewerPreprocessingHoles())
+ {
+ // Perform non-clausal simplification
+ PreprocessingPassResult res =
+ d_passes["non-clausal-simp"]->apply(&assertions);
+ if (res == PreprocessingPassResult::CONFLICT)
+ {
+ return false;
+ }
+ }
+
+ // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
+ // do the miplib trick.
+ if ( // check that option is on
+ options::arithMLTrick() &&
+ // only useful in arith
+ d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
+ // we add new assertions and need this (in practice, this
+ // restriction only disables miplib processing during
+ // re-simplification, which we don't expect to be useful anyway)
+ assertions.getRealAssertionsEnd() == assertions.size())
+ {
+ d_passes["miplib-trick"]->apply(&assertions);
+ }
+ else
+ {
+ Trace("simplify") << "SmtEnginePrivate::simplify(): "
+ << "skipping miplib pseudobooleans pass..." << endl;
+ }
+ }
+
+ Debug("smt") << " assertions : " << assertions.size() << endl;
+
+ // before ppRewrite check if only core theory for BV theory
+ d_smt.d_theoryEngine->staticInitializeBVOptions(assertions.ref());
+
+ // Theory preprocessing
+ bool doEarlyTheoryPp = !options::arithRewriteEq();
+ if (doEarlyTheoryPp)
+ {
+ d_passes["theory-preprocess"]->apply(&assertions);
+ }
+
+ // ITE simplification
+ if (options::doITESimp()
+ && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
+ {
+ PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
+ if (res == PreprocessingPassResult::CONFLICT)
+ {
+ Chat() << "...ITE simplification found unsat..." << endl;
+ return false;
+ }
+ }
+
+ Debug("smt") << " assertions : " << assertions.size() << endl;
+
+ // Unconstrained simplification
+ if (options::unconstrainedSimp())
+ {
+ d_passes["unconstrained-simplifier"]->apply(&assertions);
+ }
+
+ if (options::repeatSimp()
+ && options::simplificationMode() != options::SimplificationMode::NONE
+ && !options::unsatCores() && !options::fewerPreprocessingHoles())
+ {
+ PreprocessingPassResult res =
+ d_passes["non-clausal-simp"]->apply(&assertions);
+ if (res == PreprocessingPassResult::CONFLICT)
+ {
+ return false;
+ }
+ }
+
+ dumpAssertions("post-repeatsimp", assertions);
+ Trace("smt") << "POST repeatSimp" << endl;
+ Debug("smt") << " assertions : " << assertions.size() << endl;
+ }
+ catch (TypeCheckingExceptionPrivate& tcep)
+ {
+ // Calls to this function should have already weeded out any
+ // typechecking exceptions via (e.g.) ensureBoolean(). But a
+ // theory could still create a new expression that isn't
+ // well-typed, and we don't want the C++ runtime to abort our
+ // process without any error notice.
+ InternalError()
+ << "A bad expression was produced. Original exception follows:\n"
+ << tcep;
+ }
+ return true;
+}
+
+void ProcessAssertions::dumpAssertions(const char* key,
+ const AssertionPipeline& assertionList)
+{
+ if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
+ {
+ // Push the simplified assertions to the dump output stream
+ for (unsigned i = 0; i < assertionList.size(); ++i)
+ {
+ TNode n = assertionList[i];
+ Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+ }
+ }
+}
+
+Node ProcessAssertions::expandDefinitions(
+ TNode n,
+ unordered_map<Node, Node, NodeHashFunction>& cache,
+ bool expandOnly)
+{
+ NodeManager* nm = d_smt.d_nodeManager;
+ std::stack<std::tuple<Node, Node, bool>> worklist;
+ std::stack<Node> result;
+ worklist.push(std::make_tuple(Node(n), Node(n), false));
+ // The worklist is made of triples, each is input / original node then the
+ // output / rewritten node and finally a flag tracking whether the children
+ // have been explored (i.e. if this is a downward or upward pass).
+
+ do
+ {
+ spendResource(ResourceManager::Resource::PreprocessStep);
+
+ // n is the input / original
+ // node is the output / result
+ Node node;
+ bool childrenPushed;
+ std::tie(n, node, childrenPushed) = worklist.top();
+ worklist.pop();
+
+ // Working downwards
+ if (!childrenPushed)
+ {
+ Kind k = n.getKind();
+
+ // we can short circuit (variable) leaves
+ if (n.isVar())
+ {
+ SmtEngine::DefinedFunctionMap::const_iterator i =
+ d_smt.d_definedFunctions->find(n);
+ if (i != d_smt.d_definedFunctions->end())
+ {
+ Node f = (*i).second.getFormula();
+ // must expand its definition
+ Node fe = expandDefinitions(f, cache, expandOnly);
+ // replacement must be closed
+ if ((*i).second.getFormals().size() > 0)
+ {
+ result.push(
+ nm->mkNode(LAMBDA,
+ nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()),
+ fe));
+ continue;
+ }
+ // don't bother putting in the cache
+ result.push(fe);
+ continue;
+ }
+ // don't bother putting in the cache
+ result.push(n);
+ continue;
+ }
+
+ // maybe it's in the cache
+ unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit =
+ cache.find(n);
+ if (cacheHit != cache.end())
+ {
+ TNode ret = (*cacheHit).second;
+ result.push(ret.isNull() ? n : ret);
+ continue;
+ }
+
+ // otherwise expand it
+ bool doExpand = false;
+ if (k == APPLY_UF)
+ {
+ // Always do beta-reduction here. The reason is that there may be
+ // operators such as INTS_MODULUS in the body of the lambda that would
+ // otherwise be introduced by beta-reduction via the rewriter, but are
+ // not expanded here since the traversal in this function does not
+ // traverse the operators of nodes. Hence, we beta-reduce here to
+ // ensure terms in the body of the lambda are expanded during this
+ // call.
+ if (n.getOperator().getKind() == LAMBDA)
+ {
+ doExpand = true;
+ }
+ else
+ {
+ // We always check if this operator corresponds to a defined function.
+ doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
+ }
+ }
+ if (doExpand)
+ {
+ vector<Node> formals;
+ TNode fm;
+ if (n.getOperator().getKind() == LAMBDA)
+ {
+ TNode op = n.getOperator();
+ // lambda
+ for (unsigned i = 0; i < op[0].getNumChildren(); i++)
+ {
+ formals.push_back(op[0][i]);
+ }
+ fm = op[1];
+ }
+ else
+ {
+ // application of a user-defined symbol
+ TNode func = n.getOperator();
+ SmtEngine::DefinedFunctionMap::const_iterator i =
+ d_smt.d_definedFunctions->find(func);
+ if (i == d_smt.d_definedFunctions->end())
+ {
+ throw TypeCheckingException(
+ n.toExpr(),
+ string("Undefined function: `") + func.toString() + "'");
+ }
+ DefinedFunction def = (*i).second;
+ formals = def.getFormals();
+
+ if (Debug.isOn("expand"))
+ {
+ Debug("expand") << "found: " << n << endl;
+ Debug("expand") << " func: " << func << endl;
+ string name = func.getAttribute(expr::VarNameAttr());
+ Debug("expand") << " : \"" << name << "\"" << endl;
+ }
+ if (Debug.isOn("expand"))
+ {
+ Debug("expand") << " defn: " << def.getFunction() << endl
+ << " [";
+ if (formals.size() > 0)
+ {
+ copy(formals.begin(),
+ formals.end() - 1,
+ ostream_iterator<Node>(Debug("expand"), ", "));
+ Debug("expand") << formals.back();
+ }
+ Debug("expand") << "]" << endl
+ << " " << def.getFunction().getType() << endl
+ << " " << def.getFormula() << endl;
+ }
+
+ fm = def.getFormula();
+ }
+
+ Node instance = fm.substitute(formals.begin(),
+ formals.end(),
+ n.begin(),
+ n.begin() + formals.size());
+ Debug("expand") << "made : " << instance << endl;
+
+ Node expanded = expandDefinitions(instance, cache, expandOnly);
+ cache[n] = (n == expanded ? Node::null() : expanded);
+ result.push(expanded);
+ continue;
+ }
+ else if (!expandOnly)
+ {
+ // do not do any theory stuff if expandOnly is true
+
+ theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
+
+ Assert(t != NULL);
+ node = t->expandDefinition(n);
+ }
+
+ // the partial functions can fall through, in which case we still
+ // consider their children
+ worklist.push(std::make_tuple(
+ Node(n), node, true)); // Original and rewritten result
+
+ for (size_t i = 0; i < node.getNumChildren(); ++i)
+ {
+ worklist.push(
+ std::make_tuple(node[i],
+ node[i],
+ false)); // Rewrite the children of the result only
+ }
+ }
+ else
+ {
+ // Working upwards
+ // Reconstruct the node from it's (now rewritten) children on the stack
+
+ Debug("expand") << "cons : " << node << endl;
+ if (node.getNumChildren() > 0)
+ {
+ // cout << "cons : " << node << endl;
+ NodeBuilder<> nb(node.getKind());
+ if (node.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ Debug("expand") << "op : " << node.getOperator() << endl;
+ // cout << "op : " << node.getOperator() << endl;
+ nb << node.getOperator();
+ }
+ for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i)
+ {
+ Assert(!result.empty());
+ Node expanded = result.top();
+ result.pop();
+ // cout << "exchld : " << expanded << endl;
+ Debug("expand") << "exchld : " << expanded << endl;
+ nb << expanded;
+ }
+ node = nb;
+ }
+ // Only cache once all subterms are expanded
+ cache[n] = n == node ? Node::null() : node;
+ result.push(node);
+ }
+ } while (!worklist.empty());
+
+ AlwaysAssert(result.size() == 1);
+
+ return result.top();
+}
+
+void ProcessAssertions::collectSkolems(
+ IteSkolemMap& iskMap,
+ TNode n,
+ set<TNode>& skolemSet,
+ unordered_map<Node, bool, NodeHashFunction>& cache)
+{
+ unordered_map<Node, bool, NodeHashFunction>::iterator it;
+ it = cache.find(n);
+ if (it != cache.end())
+ {
+ return;
+ }
+
+ size_t sz = n.getNumChildren();
+ if (sz == 0)
+ {
+ if (iskMap.find(n) != iskMap.end())
+ {
+ skolemSet.insert(n);
+ }
+ cache[n] = true;
+ return;
+ }
+
+ size_t k = 0;
+ for (; k < sz; ++k)
+ {
+ collectSkolems(iskMap, n[k], skolemSet, cache);
+ }
+ cache[n] = true;
+}
+
+bool ProcessAssertions::checkForBadSkolems(
+ IteSkolemMap& iskMap,
+ TNode n,
+ TNode skolem,
+ unordered_map<Node, bool, NodeHashFunction>& cache)
+{
+ unordered_map<Node, bool, NodeHashFunction>::iterator it;
+ it = cache.find(n);
+ if (it != cache.end())
+ {
+ return (*it).second;
+ }
+
+ size_t sz = n.getNumChildren();
+ if (sz == 0)
+ {
+ IteSkolemMap::iterator iit = iskMap.find(n);
+ bool bad = false;
+ if (iit != iskMap.end())
+ {
+ if (!((*iit).first < n))
+ {
+ bad = true;
+ }
+ }
+ cache[n] = bad;
+ return bad;
+ }
+
+ size_t k = 0;
+ for (; k < sz; ++k)
+ {
+ if (checkForBadSkolems(iskMap, n[k], skolem, cache))
+ {
+ cache[n] = true;
+ return true;
+ }
+ }
+
+ cache[n] = false;
+ return false;
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file process_assertions.h
+ ** \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 The module for processing assertions for an SMT engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__PROCESS_ASSERTIONS_H
+#define CVC4__SMT__PROCESS_ASSERTIONS_H
+
+#include <map>
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/smt_engine_stats.h"
+#include "util/resource_manager.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/**
+ * Module in charge of processing assertions for an SMT engine.
+ *
+ * Its main features are:
+ * (1) apply(AssertionsPipeline&), which updates the assertions based on our
+ * preprocessing steps,
+ * (2) expandDefinitions(TNode, ...), which returns the expanded formula of a
+ * term.
+ * The method finishInit(...) must be called before these methods are called.
+ *
+ * It is designed to be agnostic to whether we are in incremental mode. That is,
+ * it processes assertions in a way that assumes that apply(...) could be
+ * applied multiple times to different sets of assertions.
+ */
+class ProcessAssertions
+{
+ /** The types for the recursive function definitions */
+ typedef context::CDList<Node> NodeList;
+ typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+ typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+
+ public:
+ ProcessAssertions(SmtEngine& smt, ResourceManager& rm);
+ ~ProcessAssertions();
+ /** Finish initialize
+ *
+ * This initializes the preprocessing passes owned by this module.
+ */
+ void finishInit(preprocessing::PreprocessingPassContext* pc);
+ /** Cleanup
+ *
+ * This deletes the processing passes owned by this module.
+ */
+ void cleanup();
+ /**
+ * Process the formulas in assertions. Returns true if there
+ * was no conflict when processing the assertions.
+ */
+ bool apply(preprocessing::AssertionPipeline& assertions);
+ /**
+ * Expand definitions in term n. Return the expanded form of n.
+ *
+ * If expandOnly is true, then the expandDefinitions function of TheoryEngine
+ * of the SmtEngine this calls is associated with is not called on subterms of
+ * n.
+ */
+ Node expandDefinitions(TNode n,
+ NodeToNodeHashMap& cache,
+ bool expandOnly = false);
+
+ private:
+ /** Reference to the SMT engine */
+ SmtEngine& d_smt;
+ /** Reference to resource manager */
+ ResourceManager& d_resourceManager;
+ /** The preprocess context */
+ preprocessing::PreprocessingPassContext* d_preprocessingPassContext;
+ /** True node */
+ Node d_true;
+ /**
+ * Map of preprocessing pass instances, mapping from names to preprocessing
+ * pass instance
+ */
+ std::unordered_map<std::string,
+ std::unique_ptr<preprocessing::PreprocessingPass>>
+ d_passes;
+ /**
+ * Number of calls of simplify assertions active.
+ */
+ unsigned d_simplifyAssertionsDepth;
+ /** recursive function definition abstractions for fmf-fun */
+ std::map<Node, TypeNode> d_fmfRecFunctionsAbs;
+ /** map to concrete definitions for fmf-fun */
+ std::map<Node, std::vector<Node>> d_fmfRecFunctionsConcrete;
+ /** List of defined recursive functions processed by fmf-fun */
+ NodeList* d_fmfRecFunctionsDefined;
+ /** Spend resource r by the resource manager of this class. */
+ void spendResource(ResourceManager::Resource r);
+ /**
+ * Perform non-clausal simplification of a Node. This involves
+ * Theory implementations, but does NOT involve the SAT solver in
+ * any way.
+ *
+ * Returns false if the formula simplifies to "false"
+ */
+ bool simplifyAssertions(preprocessing::AssertionPipeline& assertions);
+ /**
+ * Dump assertions. Print the current assertion list to the dump
+ * assertions:`key` if it is enabled.
+ */
+ void dumpAssertions(const char* key,
+ const preprocessing::AssertionPipeline& assertionList);
+ /**
+ * Helper function to fix up assertion list to restore invariants needed after
+ * ite removal.
+ */
+ void collectSkolems(IteSkolemMap& iskMap,
+ TNode n,
+ set<TNode>& skolemSet,
+ NodeToBoolHashMap& cache);
+ /**
+ * Helper function to fix up assertion list to restore invariants needed after
+ * ite removal.
+ */
+ bool checkForBadSkolems(IteSkolemMap& iskMap,
+ TNode n,
+ TNode skolem,
+ NodeToBoolHashMap& cache);
+};
+
+} // namespace smt
+} // namespace CVC4
+
+#endif
if (options::solveBVAsInt() > 0)
{
+ // not compatible with incremental
+ if (options::incrementalSolving())
+ {
+ throw OptionException(
+ "solving bitvectors as integers is currently not supported "
+ "when solving incrementally.");
+ }
+ else if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+ {
+ throw OptionException(
+ "solving bitvectors as integers is incompatible with --bool-to-bv.");
+ }
+ if (options::solveBVAsInt() > 8)
+ {
+ /**
+ * The granularity sets the size of the ITE in each element
+ * of the sum that is generated for bitwise operators.
+ * The size of the ITE is 2^{2*granularity}.
+ * Since we don't want to introduce ITEs with unbounded size,
+ * we bound the granularity.
+ */
+ throw OptionException("solve-bv-as-int accepts values from 0 to 8.");
+ }
if (logic.isTheoryEnabled(THEORY_BV))
{
logic = logic.getUnlockedCopy();
options::ufssFairnessMonotone.set(false);
options::quantEpr.set(false);
options::globalNegate.set(false);
+ options::bvAbstraction.set(false);
+ options::arithMLTrick.set(false);
}
if (logic.hasCardinalityConstraints())
{
smte.setOption("check-models", SExpr("false"));
}
}
+
+ if (options::bitblastMode() == options::BitblastMode::EAGER
+ && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV"
+ && logic.getLogicString() != "QF_ABV")
+ {
+ throw OptionException(
+ "Eager bit-blasting does not currently support theory combination. "
+ "Note that in a QF_BV problem UF symbols can be introduced for "
+ "division. "
+ "Try --bv-div-zero-const to interpret division by zero as a constant.");
+ }
}
} // namespace smt
#include "prop/prop_engine.h"
#include "smt/command.h"
#include "smt/command_list.h"
+#include "smt/defined_function.h"
#include "smt/logic_request.h"
#include "smt/managed_ostreams.h"
#include "smt/model_blocker.h"
#include "smt/model_core_builder.h"
+#include "smt/process_assertions.h"
#include "smt/set_defaults.h"
#include "smt/smt_engine_scope.h"
+#include "smt/smt_engine_stats.h"
#include "smt/term_formula_removal.h"
#include "smt/update_ostream.h"
#include "smt_util/boolean_simplification.h"
commands.clear();
}
-/** Useful for counting the number of recursive calls. */
-class ScopeCounter {
-private:
- unsigned& d_depth;
-public:
- ScopeCounter(unsigned& d) : d_depth(d) {
- ++d_depth;
- }
- ~ScopeCounter(){
- --d_depth;
- }
-};
-
-/**
- * Representation of a defined function. We keep these around in
- * SmtEngine to permit expanding definitions late (and lazily), to
- * support getValue() over defined functions, to support user output
- * in terms of defined functions, etc.
- */
-class DefinedFunction {
- Node d_func;
- vector<Node> d_formals;
- Node d_formula;
-public:
- DefinedFunction() {}
- DefinedFunction(Node func, vector<Node>& formals, Node formula)
- : d_func(func), d_formals(formals), d_formula(formula)
- {
- }
- Node getFunction() const { return d_func; }
- vector<Node> getFormals() const { return d_formals; }
- Node getFormula() const { return d_formula; }
-};/* class DefinedFunction */
-
-struct SmtEngineStatistics {
- /** time spent in definition-expansion */
- TimerStat d_definitionExpansionTime;
- /** number of constant propagations found during nonclausal simp */
- IntStat d_numConstantProps;
- /** time spent converting to CNF */
- TimerStat d_cnfConversionTime;
- /** Num of assertions before ite removal */
- IntStat d_numAssertionsPre;
- /** Num of assertions after ite removal */
- IntStat d_numAssertionsPost;
- /** Size of all proofs generated */
- IntStat d_proofsSize;
- /** time spent in checkModel() */
- TimerStat d_checkModelTime;
- /** time spent checking the proof with LFSC */
- TimerStat d_lfscCheckProofTime;
- /** time spent in checkUnsatCore() */
- TimerStat d_checkUnsatCoreTime;
- /** time spent in PropEngine::checkSat() */
- TimerStat d_solveTime;
- /** time spent in pushing/popping */
- TimerStat d_pushPopTime;
- /** time spent in processAssertions() */
- TimerStat d_processAssertionsTime;
-
- /** Has something simplified to false? */
- IntStat d_simplifiedToFalse;
- /** Number of resource units spent. */
- ReferenceStat<uint64_t> d_resourceUnitsUsed;
-
- SmtEngineStatistics()
- : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
- d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
- d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
- d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
- d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
- d_proofsSize("smt::SmtEngine::proofsSize", 0),
- d_checkModelTime("smt::SmtEngine::checkModelTime"),
- d_lfscCheckProofTime("smt::SmtEngine::lfscCheckProofTime"),
- d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
- d_solveTime("smt::SmtEngine::solveTime"),
- d_pushPopTime("smt::SmtEngine::pushPopTime"),
- d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
- d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
- d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
- {
- smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
- smtStatisticsRegistry()->registerStat(&d_numConstantProps);
- smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
- smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
- smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
- smtStatisticsRegistry()->registerStat(&d_proofsSize);
- smtStatisticsRegistry()->registerStat(&d_checkModelTime);
- smtStatisticsRegistry()->registerStat(&d_lfscCheckProofTime);
- smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
- smtStatisticsRegistry()->registerStat(&d_solveTime);
- smtStatisticsRegistry()->registerStat(&d_pushPopTime);
- smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
- smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
- smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
- }
-
- ~SmtEngineStatistics() {
- smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
- smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
- smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
- smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
- smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
- smtStatisticsRegistry()->unregisterStat(&d_proofsSize);
- smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
- smtStatisticsRegistry()->unregisterStat(&d_lfscCheckProofTime);
- smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
- smtStatisticsRegistry()->unregisterStat(&d_solveTime);
- smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
- smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
- smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
- smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
- }
-};/* struct SmtEngineStatistics */
-
-
class SoftResourceOutListener : public Listener {
public:
SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
*/
NodeToNodeHashMap d_abstractValues;
- /** Number of calls of simplify assertions active.
- */
- unsigned d_simplifyAssertionsDepth;
-
/** TODO: whether certain preprocess steps are necessary */
//bool d_needsExpandDefs;
+ /** The preprocessing pass context */
+ std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
+
+ /** Process assertions module */
+ ProcessAssertions d_processor;
+
//------------------------------- expression names
/** mapping from expressions to name */
context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
CDO<bool> d_sygusConjectureStale;
/*------------------- end of sygus utils ------------------*/
- private:
- std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
-
- /**
- * Map of preprocessing pass instances, mapping from names to preprocessing
- * pass instance
- */
- std::unordered_map<std::string, std::unique_ptr<PreprocessingPass>> d_passes;
-
- /**
- * Helper function to fix up assertion list to restore invariants needed after
- * ite removal.
- */
- void collectSkolems(TNode n, set<TNode>& skolemSet, NodeToBoolHashMap& cache);
-
- /**
- * Helper function to fix up assertion list to restore invariants needed after
- * ite removal.
- */
- bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
-
- /**
- * Perform non-clausal simplification of a Node. This involves
- * Theory implementations, but does NOT involve the SAT solver in
- * any way.
- *
- * Returns false if the formula simplifies to "false"
- */
- bool simplifyAssertions();
-
public:
SmtEnginePrivate(SmtEngine& smt)
: d_smt(smt),
+ d_resourceManager(NodeManager::currentResourceManager()),
d_managedRegularChannel(),
d_managedDiagnosticChannel(),
d_managedDumpChannel(),
d_fakeContext(),
d_abstractValueMap(&d_fakeContext),
d_abstractValues(),
- d_simplifyAssertionsDepth(0),
+ d_processor(smt, *d_resourceManager),
// d_needsExpandDefs(true), //TODO?
d_exprNames(smt.getUserContext()),
d_iteRemover(smt.getUserContext()),
{
d_smt.d_nodeManager->subscribeEvents(this);
d_true = NodeManager::currentNM()->mkConst(true);
- d_resourceManager = NodeManager::currentResourceManager();
d_listenerRegistrations->add(d_resourceManager->registerSoftListener(
new SoftResourceOutListener(d_smt)));
d_smt.d_nodeManager->unsubscribeEvents(this);
}
- void cleanupPreprocessingPasses() { d_passes.clear(); }
-
ResourceManager* getResourceManager() { return d_resourceManager; }
void spendResource(ResourceManager::Resource r)
d_resourceManager->spendResource(r);
}
+ ProcessAssertions* getProcessAssertions() { return &d_processor; }
+
void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
{
DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
bool inInput = true,
bool isAssumption = false,
bool maybeHasFv = false);
-
- /** Expand definitions in n. */
- Node expandDefinitions(TNode n,
- NodeToNodeHashMap& cache,
- bool expandOnly = false);
-
/**
* Simplify node "in" by expanding definitions and applying any
* substitutions learned from preprocessing.
// Substitute out any abstract values in ex.
// Expand definitions.
NodeToNodeHashMap cache;
- Node n = expandDefinitions(in, cache).toExpr();
+ Node n = d_processor.expandDefinitions(in, cache).toExpr();
// Make sure we've done all preprocessing, etc.
Assert(d_assertions.size() == 0);
return applySubstitutions(n).toExpr();
d_proofManager(nullptr),
d_rewriter(new theory::Rewriter()),
d_definedFunctions(nullptr),
- d_fmfRecFunctionsDefined(nullptr),
d_assertionList(nullptr),
d_assignments(nullptr),
d_modelGlobalCommands(),
#endif
d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
- d_fmfRecFunctionsDefined = new (true) NodeList(getUserContext());
d_modelCommands = new (true) smt::CommandList(getUserContext());
}
}
d_definedFunctions->deleteSelf();
- d_fmfRecFunctionsDefined->deleteSelf();
//destroy all passes before destroying things that they refer to
- d_private->cleanupPreprocessingPasses();
+ d_private->getProcessAssertions()->cleanup();
// d_proofManager is always created when proofs are enabled at configure
// time. Because of this, this code should not be wrapped in PROOF() which
void SmtEnginePrivate::finishInit()
{
- PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
d_preprocessingPassContext.reset(new PreprocessingPassContext(
&d_smt, d_resourceManager, &d_iteRemover, &d_propagator));
- // TODO: this will likely change when we add support for actually assembling
- // preprocessing pipelines. For now, we just create an instance of each
- // available preprocessing pass.
- std::vector<std::string> passNames = ppReg.getAvailablePasses();
- for (const std::string& passName : passNames)
- {
- d_passes[passName].reset(
- ppReg.createPass(d_preprocessingPassContext.get(), passName));
- }
-}
-
-Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
-{
- stack<std::tuple<Node, Node, bool>> worklist;
- stack<Node> result;
- worklist.push(std::make_tuple(Node(n), Node(n), false));
- // The worklist is made of triples, each is input / original node then the output / rewritten node
- // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
- // or upward pass).
-
- do {
- spendResource(ResourceManager::Resource::PreprocessStep);
-
- // n is the input / original
- // node is the output / result
- Node node;
- bool childrenPushed;
- std::tie(n, node, childrenPushed) = worklist.top();
- worklist.pop();
-
- // Working downwards
- if(!childrenPushed) {
- Kind k = n.getKind();
-
- // we can short circuit (variable) leaves
- if(n.isVar()) {
- SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
- if(i != d_smt.d_definedFunctions->end()) {
- Node f = (*i).second.getFormula();
- // must expand its definition
- Node fe = expandDefinitions(f, cache, expandOnly);
- // replacement must be closed
- if((*i).second.getFormals().size() > 0) {
- result.push(d_smt.d_nodeManager->mkNode(
- kind::LAMBDA,
- d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST,
- (*i).second.getFormals()),
- fe));
- continue;
- }
- // don't bother putting in the cache
- result.push(fe);
- continue;
- }
- // don't bother putting in the cache
- result.push(n);
- continue;
- }
-
- // maybe it's in the cache
- unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
- if(cacheHit != cache.end()) {
- TNode ret = (*cacheHit).second;
- result.push(ret.isNull() ? n : ret);
- continue;
- }
-
- // otherwise expand it
- bool doExpand = false;
- if (k == kind::APPLY_UF)
- {
- // Always do beta-reduction here. The reason is that there may be
- // operators such as INTS_MODULUS in the body of the lambda that would
- // otherwise be introduced by beta-reduction via the rewriter, but are
- // not expanded here since the traversal in this function does not
- // traverse the operators of nodes. Hence, we beta-reduce here to
- // ensure terms in the body of the lambda are expanded during this
- // call.
- if (n.getOperator().getKind() == kind::LAMBDA)
- {
- doExpand = true;
- }
- else
- {
- // We always check if this operator corresponds to a defined function.
- doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
- }
- }
- if (doExpand) {
- vector<Node> formals;
- TNode fm;
- if( n.getOperator().getKind() == kind::LAMBDA ){
- TNode op = n.getOperator();
- // lambda
- for( unsigned i=0; i<op[0].getNumChildren(); i++ ){
- formals.push_back( op[0][i] );
- }
- fm = op[1];
- }else{
- // application of a user-defined symbol
- TNode func = n.getOperator();
- SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func);
- if(i == d_smt.d_definedFunctions->end()) {
- throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
- }
- DefinedFunction def = (*i).second;
- formals = def.getFormals();
-
- if(Debug.isOn("expand")) {
- Debug("expand") << "found: " << n << endl;
- Debug("expand") << " func: " << func << endl;
- string name = func.getAttribute(expr::VarNameAttr());
- Debug("expand") << " : \"" << name << "\"" << endl;
- }
- if(Debug.isOn("expand")) {
- Debug("expand") << " defn: " << def.getFunction() << endl
- << " [";
- if(formals.size() > 0) {
- copy( formals.begin(), formals.end() - 1,
- ostream_iterator<Node>(Debug("expand"), ", ") );
- Debug("expand") << formals.back();
- }
- Debug("expand") << "]" << endl
- << " " << def.getFunction().getType() << endl
- << " " << def.getFormula() << endl;
- }
-
- fm = def.getFormula();
- }
-
- Node instance = fm.substitute(formals.begin(),
- formals.end(),
- n.begin(),
- n.begin() + formals.size());
- Debug("expand") << "made : " << instance << endl;
-
- Node expanded = expandDefinitions(instance, cache, expandOnly);
- cache[n] = (n == expanded ? Node::null() : expanded);
- result.push(expanded);
- continue;
-
- } else if(! expandOnly) {
- // do not do any theory stuff if expandOnly is true
-
- theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
-
- Assert(t != NULL);
- node = t->expandDefinition(n);
- }
-
- // the partial functions can fall through, in which case we still
- // consider their children
- worklist.push(std::make_tuple(
- Node(n), node, true)); // Original and rewritten result
-
- for(size_t i = 0; i < node.getNumChildren(); ++i) {
- worklist.push(
- std::make_tuple(node[i],
- node[i],
- false)); // Rewrite the children of the result only
- }
-
- } else {
- // Working upwards
- // Reconstruct the node from it's (now rewritten) children on the stack
-
- Debug("expand") << "cons : " << node << endl;
- if(node.getNumChildren()>0) {
- //cout << "cons : " << node << endl;
- NodeBuilder<> nb(node.getKind());
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- Debug("expand") << "op : " << node.getOperator() << endl;
- //cout << "op : " << node.getOperator() << endl;
- nb << node.getOperator();
- }
- for(size_t i = 0; i < node.getNumChildren(); ++i) {
- Assert(!result.empty());
- Node expanded = result.top();
- result.pop();
- //cout << "exchld : " << expanded << endl;
- Debug("expand") << "exchld : " << expanded << endl;
- nb << expanded;
- }
- node = nb;
- }
- cache[n] = n == node ? Node::null() : node; // Only cache once all subterms are expanded
- result.push(node);
- }
- } while(!worklist.empty());
-
- AlwaysAssert(result.size() == 1);
-
- return result.top();
-}
-
-// do dumping (before/after any preprocessing pass)
-static void dumpAssertions(const char* key,
- const AssertionPipeline& assertionList) {
- if( Dump.isOn("assertions") &&
- Dump.isOn(string("assertions:") + key) ) {
- // Push the simplified assertions to the dump output stream
- for(unsigned i = 0; i < assertionList.size(); ++ i) {
- TNode n = assertionList[i];
- Dump("assertions") << AssertCommand(Expr(n.toExpr()));
- }
- }
-}
-
-// returns false if simplification led to "false"
-bool SmtEnginePrivate::simplifyAssertions()
-{
- spendResource(ResourceManager::Resource::PreprocessStep);
- Assert(d_smt.d_pendingPops == 0);
- try {
- ScopeCounter depth(d_simplifyAssertionsDepth);
-
- Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
-
- if (options::simplificationMode() != options::SimplificationMode::NONE)
- {
- if (!options::unsatCores() && !options::fewerPreprocessingHoles())
- {
- // Perform non-clausal simplification
- PreprocessingPassResult res =
- d_passes["non-clausal-simp"]->apply(&d_assertions);
- if (res == PreprocessingPassResult::CONFLICT)
- {
- return false;
- }
- }
-
- // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
- // do the miplib trick.
- if ( // check that option is on
- options::arithMLTrick() &&
- // miplib rewrites aren't safe in incremental mode
- !options::incrementalSolving() &&
- // only useful in arith
- d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
- // we add new assertions and need this (in practice, this
- // restriction only disables miplib processing during
- // re-simplification, which we don't expect to be useful anyway)
- d_assertions.getRealAssertionsEnd() == d_assertions.size())
- {
- d_passes["miplib-trick"]->apply(&d_assertions);
- } else {
- Trace("simplify") << "SmtEnginePrivate::simplify(): "
- << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;
- }
- }
-
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
- // before ppRewrite check if only core theory for BV theory
- d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref());
-
- // Theory preprocessing
- bool doEarlyTheoryPp = !options::arithRewriteEq();
- if (doEarlyTheoryPp)
- {
- d_passes["theory-preprocess"]->apply(&d_assertions);
- }
-
- // ITE simplification
- if (options::doITESimp()
- && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
- {
- PreprocessingPassResult res = d_passes["ite-simp"]->apply(&d_assertions);
- if (res == PreprocessingPassResult::CONFLICT)
- {
- Chat() << "...ITE simplification found unsat..." << endl;
- return false;
- }
- }
-
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
- // Unconstrained simplification
- if(options::unconstrainedSimp()) {
- d_passes["unconstrained-simplifier"]->apply(&d_assertions);
- }
-
- if (options::repeatSimp()
- && options::simplificationMode() != options::SimplificationMode::NONE
- && !options::unsatCores() && !options::fewerPreprocessingHoles())
- {
- PreprocessingPassResult res =
- d_passes["non-clausal-simp"]->apply(&d_assertions);
- if (res == PreprocessingPassResult::CONFLICT)
- {
- return false;
- }
- }
-
- dumpAssertions("post-repeatsimp", d_assertions);
- Trace("smt") << "POST repeatSimp" << endl;
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
- } catch(TypeCheckingExceptionPrivate& tcep) {
- // Calls to this function should have already weeded out any
- // typechecking exceptions via (e.g.) ensureBoolean(). But a
- // theory could still create a new expression that isn't
- // well-typed, and we don't want the C++ runtime to abort our
- // process without any error notice.
- InternalError()
- << "A bad expression was produced. Original exception follows:\n"
- << tcep;
- }
- return true;
+ // initialize the preprocessing passes
+ d_processor.finishInit(d_preprocessingPassContext.get());
}
Result SmtEngine::check() {
return m;
}
-void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
-{
- unordered_map<Node, bool, NodeHashFunction>::iterator it;
- it = cache.find(n);
- if (it != cache.end()) {
- return;
- }
-
- size_t sz = n.getNumChildren();
- if (sz == 0) {
- if (getIteSkolemMap().find(n) != getIteSkolemMap().end())
- {
- skolemSet.insert(n);
- }
- cache[n] = true;
- return;
- }
-
- size_t k = 0;
- for (; k < sz; ++k) {
- collectSkolems(n[k], skolemSet, cache);
- }
- cache[n] = true;
-}
-
-bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
-{
- unordered_map<Node, bool, NodeHashFunction>::iterator it;
- it = cache.find(n);
- if (it != cache.end()) {
- return (*it).second;
- }
-
- size_t sz = n.getNumChildren();
- if (sz == 0) {
- IteSkolemMap::iterator iit = getIteSkolemMap().find(n);
- bool bad = false;
- if (iit != getIteSkolemMap().end())
- {
- if (!((*iit).first < n))
- {
- bad = true;
- }
- }
- cache[n] = bad;
- return bad;
- }
-
- size_t k = 0;
- for (; k < sz; ++k) {
- if (checkForBadSkolems(n[k], skolem, cache)) {
- cache[n] = true;
- return true;
- }
- }
-
- cache[n] = false;
- return false;
-}
-
void SmtEnginePrivate::processAssertions() {
TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
spendResource(ResourceManager::Resource::PreprocessStep);
Assert(d_smt.d_fullyInited);
Assert(d_smt.d_pendingPops == 0);
- SubstitutionMap& top_level_substs =
- d_preprocessingPassContext->getTopLevelSubstitutions();
-
- // Dump the assertions
- dumpAssertions("pre-everything", d_assertions);
-
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl;
- Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
-
- Debug("smt") << "#Assertions : " << d_assertions.size() << endl;
- Debug("smt") << "#Assumptions: " << d_assertions.getNumAssumptions() << endl;
if (d_assertions.size() == 0) {
// nothing to do
return;
}
-
- if (options::bvGaussElim())
- {
- d_passes["bv-gauss"]->apply(&d_assertions);
- }
-
if (d_assertionsProcessed && options::incrementalSolving()) {
// TODO(b/1255): Substitutions in incremental mode should be managed with a
// proper data structure.
d_assertions.disableStoreSubstsInAsserts();
}
- // Add dummy assertion in last position - to be used as a
- // placeholder for any new assertions to get added
- d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
- // any assertions added beyond realAssertionsEnd must NOT affect the
- // equisatisfiability
- d_assertions.updateRealAssertionsEnd();
-
- // Assertions are NOT guaranteed to be rewritten by this point
-
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl;
- dumpAssertions("pre-definition-expansion", d_assertions);
- {
- Chat() << "expanding definitions..." << endl;
- Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
- TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
- unordered_map<Node, Node, NodeHashFunction> cache;
- for(unsigned i = 0; i < d_assertions.size(); ++ i) {
- d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
- }
- }
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
- dumpAssertions("post-definition-expansion", d_assertions);
-
- // save the assertions now
- THEORY_PROOF
- (
- for (unsigned i = 0; i < d_assertions.size(); ++i) {
- ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr());
- }
- );
-
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
- if (options::globalNegate())
- {
- // global negation of the formula
- d_passes["global-negate"]->apply(&d_assertions);
- d_smt.d_globalNegation = !d_smt.d_globalNegation;
- }
-
- if( options::nlExtPurify() ){
- d_passes["nl-ext-purify"]->apply(&d_assertions);
- }
-
- if (options::solveRealAsInt()) {
- d_passes["real-to-int"]->apply(&d_assertions);
- }
-
- if (options::solveIntAsBV() > 0)
- {
- d_passes["int-to-bv"]->apply(&d_assertions);
- }
-
- if (options::bitblastMode() == options::BitblastMode::EAGER
- && !d_smt.d_logic.isPure(THEORY_BV)
- && d_smt.d_logic.getLogicString() != "QF_UFBV"
- && d_smt.d_logic.getLogicString() != "QF_ABV")
- {
- throw ModalException("Eager bit-blasting does not currently support theory combination. "
- "Note that in a QF_BV problem UF symbols can be introduced for division. "
- "Try --bv-div-zero-const to interpret division by zero as a constant.");
- }
-
- if (options::ackermann())
- {
- d_passes["ackermann"]->apply(&d_assertions);
- }
-
- if (options::bvAbstraction() && !options::incrementalSolving())
- {
- d_passes["bv-abstraction"]->apply(&d_assertions);
- }
-
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
- bool noConflict = true;
-
- if (options::extRewPrep())
- {
- d_passes["ext-rew-pre"]->apply(&d_assertions);
- }
-
- // Unconstrained simplification
- if(options::unconstrainedSimp()) {
- d_passes["rewrite"]->apply(&d_assertions);
- d_passes["unconstrained-simplifier"]->apply(&d_assertions);
- }
-
- if(options::bvIntroducePow2())
- {
- d_passes["bv-intro-pow2"]->apply(&d_assertions);
- }
-
- // Since this pass is not robust for the information tracking necessary for
- // unsat cores, it's only applied if we are not doing unsat core computation
- if (!options::unsatCores())
- {
- d_passes["apply-substs"]->apply(&d_assertions);
- }
-
- // Assertions MUST BE guaranteed to be rewritten by this point
- d_passes["rewrite"]->apply(&d_assertions);
-
- // Lift bit-vectors of size 1 to bool
- if (options::bitvectorToBool())
- {
- d_passes["bv-to-bool"]->apply(&d_assertions);
- }
- if (options::solveBVAsInt() > 0)
- {
- if (options::incrementalSolving())
- {
- throw ModalException(
- "solving bitvectors as integers is currently not supported "
- "when solving incrementally.");
- } else if (options::boolToBitvector() != options::BoolToBVMode::OFF) {
- throw ModalException(
- "solving bitvectors as integers is incompatible with --bool-to-bv.");
- }
- else if (options::solveBVAsInt() > 8)
- {
- /**
- * The granularity sets the size of the ITE in each element
- * of the sum that is generated for bitwise operators.
- * The size of the ITE is 2^{2*granularity}.
- * Since we don't want to introduce ITEs with unbounded size,
- * we bound the granularity.
- */
- throw ModalException("solve-bv-as-int accepts values from 0 to 8.");
- }
- else
- {
- d_passes["bv-to-int"]->apply(&d_assertions);
- }
- }
-
- // Convert non-top-level Booleans to bit-vectors of size 1
- if (options::boolToBitvector() != options::BoolToBVMode::OFF)
- {
- d_passes["bool-to-bv"]->apply(&d_assertions);
- }
- if(options::sepPreSkolemEmp()) {
- d_passes["sep-skolem-emp"]->apply(&d_assertions);
- }
-
- if( d_smt.d_logic.isQuantified() ){
- //remove rewrite rules, apply pre-skolemization to existential quantifiers
- d_passes["quantifiers-preprocess"]->apply(&d_assertions);
- if( options::macrosQuant() ){
- //quantifiers macro expansion
- d_passes["quantifier-macros"]->apply(&d_assertions);
- }
-
- //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
- if( options::fmfFunWellDefined() ){
- quantifiers::FunDefFmf fdf;
- Assert(d_smt.d_fmfRecFunctionsDefined != NULL);
- //must carry over current definitions (for incremental)
- for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin();
- fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {
- Node f = (*fit);
- Assert(d_smt.d_fmfRecFunctionsAbs.find(f)
- != d_smt.d_fmfRecFunctionsAbs.end());
- TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f];
- fdf.d_sorts[f] = ft;
- std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f );
- Assert(fcit != d_smt.d_fmfRecFunctionsConcrete.end());
- for( unsigned j=0; j<fcit->second.size(); j++ ){
- fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
- }
- }
- fdf.simplify( d_assertions.ref() );
- //must store new definitions (for incremental)
- for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
- Node f = fdf.d_funcs[i];
- d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
- d_smt.d_fmfRecFunctionsConcrete[f].clear();
- for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
- d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] );
- }
- d_smt.d_fmfRecFunctionsDefined->push_back( f );
- }
- }
- }
-
- if( options::sortInference() || options::ufssFairnessMonotone() ){
- d_passes["sort-inference"]->apply(&d_assertions);
- }
-
- if( options::pbRewrites() ){
- d_passes["pseudo-boolean-processor"]->apply(&d_assertions);
- }
-
- // rephrasing normal inputs as sygus problems
- if (!d_smt.d_isInternalSubsolver)
- {
- if (options::sygusInference())
- {
- d_passes["sygus-infer"]->apply(&d_assertions);
- }
- else if (options::sygusRewSynthInput())
- {
- // do candidate rewrite rule synthesis
- d_passes["synth-rr"]->apply(&d_assertions);
- }
- }
-
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;
- dumpAssertions("pre-simplify", d_assertions);
- Chat() << "simplifying assertions..." << endl;
- noConflict = simplifyAssertions();
- if(!noConflict){
- ++(d_smt.d_stats->d_simplifiedToFalse);
- }
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl;
- dumpAssertions("post-simplify", d_assertions);
-
- if(options::doStaticLearning()) {
- d_passes["static-learning"]->apply(&d_assertions);
- }
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
- {
- d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
- d_passes["ite-removal"]->apply(&d_assertions);
- // This is needed because when solving incrementally, removeITEs may introduce
- // skolems that were solved for earlier and thus appear in the substitution
- // map.
- d_passes["apply-substs"]->apply(&d_assertions);
- d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
- }
-
- dumpAssertions("pre-repeat-simplify", d_assertions);
- if(options::repeatSimp()) {
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
- Chat() << "re-simplifying assertions..." << endl;
- ScopeCounter depth(d_simplifyAssertionsDepth);
- noConflict &= simplifyAssertions();
- if (noConflict) {
- // Need to fix up assertion list to maintain invariants:
- // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced
- // during ite removal.
- // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
-
- // cache for expression traversal
- unordered_map<Node, bool, NodeHashFunction> cache;
-
- // First, find all skolems that appear in the substitution map - their associated iteExpr will need
- // to be moved to the main assertion set
- set<TNode> skolemSet;
- SubstitutionMap::iterator pos = top_level_substs.begin();
- for (; pos != top_level_substs.end(); ++pos)
- {
- collectSkolems((*pos).first, skolemSet, cache);
- collectSkolems((*pos).second, skolemSet, cache);
- }
-
- // We need to ensure:
- // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
- // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
- // If either of these is violated, we must add iteExpr as a proper assertion
- IteSkolemMap::iterator it = getIteSkolemMap().begin();
- IteSkolemMap::iterator iend = getIteSkolemMap().end();
- NodeBuilder<> builder(kind::AND);
- builder << d_assertions[d_assertions.getRealAssertionsEnd() - 1];
- vector<TNode> toErase;
- for (; it != iend; ++it) {
- if (skolemSet.find((*it).first) == skolemSet.end()) {
- TNode iteExpr = d_assertions[(*it).second];
- if (iteExpr.getKind() == kind::ITE &&
- iteExpr[1].getKind() == kind::EQUAL &&
- iteExpr[1][0] == (*it).first &&
- iteExpr[2].getKind() == kind::EQUAL &&
- iteExpr[2][0] == (*it).first) {
- cache.clear();
- bool bad = checkForBadSkolems(iteExpr[0], (*it).first, cache);
- bad = bad || checkForBadSkolems(iteExpr[1][1], (*it).first, cache);
- bad = bad || checkForBadSkolems(iteExpr[2][1], (*it).first, cache);
- if (!bad) {
- continue;
- }
- }
- }
- // Move this iteExpr into the main assertions
- builder << d_assertions[(*it).second];
- d_assertions[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
- toErase.push_back((*it).first);
- }
- if(builder.getNumChildren() > 1) {
- while (!toErase.empty()) {
- getIteSkolemMap().erase(toErase.back());
- toErase.pop_back();
- }
- d_assertions[d_assertions.getRealAssertionsEnd() - 1] =
- Rewriter::rewrite(Node(builder));
- }
- // TODO(b/1256): For some reason this is needed for some benchmarks, such as
- // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
- d_passes["ite-removal"]->apply(&d_assertions);
- d_passes["apply-substs"]->apply(&d_assertions);
- // Assert(iteRewriteAssertionsEnd == d_assertions.size());
- }
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
- }
- dumpAssertions("post-repeat-simplify", d_assertions);
-
- if (options::ufHo())
- {
- d_passes["ho-elim"]->apply(&d_assertions);
- }
-
- // begin: INVARIANT to maintain: no reordering of assertions or
- // introducing new ones
-#ifdef CVC4_ASSERTIONS
- unsigned iteRewriteAssertionsEnd = d_assertions.size();
-#endif
-
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
- Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
- d_passes["theory-preprocess"]->apply(&d_assertions);
-
- if (options::bitblastMode() == options::BitblastMode::EAGER)
- {
- d_passes["bv-eager-atoms"]->apply(&d_assertions);
- }
+ // process the assertions
+ bool noConflict = d_processor.apply(d_assertions);
//notify theory engine new preprocessed assertions
d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() );
if (noConflict)
{
Chat() << "pushing to decision engine..." << endl;
- Assert(iteRewriteAssertionsEnd == d_assertions.size());
d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions);
}
// end: INVARIANT to maintain: no reordering of assertions or
// introducing new ones
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
- dumpAssertions("post-everything", d_assertions);
-
// if incremental, compute which variables are assigned
if (options::incrementalSolving())
{
}
unordered_map<Node, Node, NodeHashFunction> cache;
- Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
+ Node n = d_private->getProcessAssertions()->expandDefinitions(
+ Node::fromExpr(e), cache, /* expandOnly = */ true);
n = postprocess(n, TypeNode::fromType(e.getType()));
return n.toExpr();
// Expand, then normalize
unordered_map<Node, Node, NodeHashFunction> cache;
- n = d_private->expandDefinitions(n, cache);
+ n = d_private->getProcessAssertions()->expandDefinitions(n, cache);
// There are two ways model values for terms are computed (for historical
// reasons). One way is that used in check-model; the other is that
// used by the Model classes. It's not clear to me exactly how these
// Expand, then normalize
unordered_map<Node, Node, NodeHashFunction> cache;
- Node n = d_private->expandDefinitions(as, cache);
+ Node n = d_private->getProcessAssertions()->expandDefinitions(as, cache);
n = Rewriter::rewrite(n);
Trace("smt") << "--- getting value of " << n << endl;
for (const Expr& e : easserts)
{
Node ea = Node::fromExpr(e);
- Node eae = d_private->expandDefinitions(ea, cache);
+ Node eae = d_private->getProcessAssertions()->expandDefinitions(ea, cache);
eassertsProc.push_back(eae.toExpr());
}
return eassertsProc;
// Apply any define-funs from the problem.
{
unordered_map<Node, Node, NodeHashFunction> cache;
- n = d_private->expandDefinitions(n, cache);
+ n = d_private->getProcessAssertions()->expandDefinitions(n, cache);
}
Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
Trace("check-synth-sol") << "Retrieving assertion " << *i << "\n";
Node assertion = Node::fromExpr(*i);
// Apply any define-funs from the problem.
- assertion = d_private->expandDefinitions(assertion, cache);
+ assertion =
+ d_private->getProcessAssertions()->expandDefinitions(assertion, cache);
Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << assertion
<< endl;
Trace("check-synth-sol") << "Expanded assertion " << assertion << "\n";
Node conjn = Node::fromExpr(conj);
// must expand definitions
std::unordered_map<Node, Node, NodeHashFunction> cache;
- conjn = d_private->expandDefinitions(conjn, cache);
+ conjn = d_private->getProcessAssertions()->expandDefinitions(conjn, cache);
// now negate
conjn = conjn.negate();
d_abdConj = conjn.toExpr();
struct SmtEngineStatistics;
class SmtEnginePrivate;
class SmtScope;
- class BooleanTermConverter;
+ class ProcessAssertions;
ProofManager* currentProofManager();
friend class ::CVC4::preprocessing::PreprocessingPassContext;
friend class ::CVC4::smt::SmtEnginePrivate;
friend class ::CVC4::smt::SmtScope;
- friend class ::CVC4::smt::BooleanTermConverter;
+ friend class ::CVC4::smt::ProcessAssertions;
friend ProofManager* ::CVC4::smt::currentProofManager();
friend class ::CVC4::LogicRequest;
friend class ::CVC4::Model; // to access d_modelCommands
*/
Expr d_abdConj;
- /** recursive function definition abstractions for --fmf-fun */
- std::map<Node, TypeNode> d_fmfRecFunctionsAbs;
- std::map<Node, std::vector<Node> > d_fmfRecFunctionsConcrete;
- NodeList* d_fmfRecFunctionsDefined;
-
/**
* The assertion list (before any conversion) for supporting
* getAssertions(). Only maintained if in interactive mode.
--- /dev/null
+/********************* */
+/*! \file smt_engine_stats.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 Implementation of statistics for SMT engine
+ **/
+
+#include "smt/smt_engine_stats.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace smt {
+
+SmtEngineStatistics::SmtEngineStatistics()
+ : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
+ d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
+ d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
+ d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
+ d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
+ d_proofsSize("smt::SmtEngine::proofsSize", 0),
+ d_checkModelTime("smt::SmtEngine::checkModelTime"),
+ d_lfscCheckProofTime("smt::SmtEngine::lfscCheckProofTime"),
+ d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
+ d_solveTime("smt::SmtEngine::solveTime"),
+ d_pushPopTime("smt::SmtEngine::pushPopTime"),
+ d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
+ d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
+ d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
+{
+ smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
+ smtStatisticsRegistry()->registerStat(&d_numConstantProps);
+ smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
+ smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
+ smtStatisticsRegistry()->registerStat(&d_proofsSize);
+ smtStatisticsRegistry()->registerStat(&d_checkModelTime);
+ smtStatisticsRegistry()->registerStat(&d_lfscCheckProofTime);
+ smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
+ smtStatisticsRegistry()->registerStat(&d_solveTime);
+ smtStatisticsRegistry()->registerStat(&d_pushPopTime);
+ smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
+ smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
+ smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
+}
+
+SmtEngineStatistics::~SmtEngineStatistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
+ smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
+ smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
+ smtStatisticsRegistry()->unregisterStat(&d_proofsSize);
+ smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
+ smtStatisticsRegistry()->unregisterStat(&d_lfscCheckProofTime);
+ smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
+ smtStatisticsRegistry()->unregisterStat(&d_solveTime);
+ smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
+ smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
+ smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file smt_engine_stats.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 Statistics for SMT engine
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__SMT_ENGINE_STATS_H
+#define CVC4__SMT__SMT_ENGINE_STATS_H
+
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace smt {
+
+struct SmtEngineStatistics
+{
+ SmtEngineStatistics();
+ ~SmtEngineStatistics();
+ /** time spent in definition-expansion */
+ TimerStat d_definitionExpansionTime;
+ /** number of constant propagations found during nonclausal simp */
+ IntStat d_numConstantProps;
+ /** time spent converting to CNF */
+ TimerStat d_cnfConversionTime;
+ /** Number of assertions before ite removal */
+ IntStat d_numAssertionsPre;
+ /** Number of assertions after ite removal */
+ IntStat d_numAssertionsPost;
+ /** Size of all proofs generated */
+ IntStat d_proofsSize;
+ /** time spent in checkModel() */
+ TimerStat d_checkModelTime;
+ /** time spent checking the proof with LFSC */
+ TimerStat d_lfscCheckProofTime;
+ /** time spent in checkUnsatCore() */
+ TimerStat d_checkUnsatCoreTime;
+ /** time spent in PropEngine::checkSat() */
+ TimerStat d_solveTime;
+ /** time spent in pushing/popping */
+ TimerStat d_pushPopTime;
+ /** time spent in processAssertions() */
+ TimerStat d_processAssertionsTime;
+
+ /** Has something simplified to false? */
+ IntStat d_simplifiedToFalse;
+ /** Number of resource units spent. */
+ ReferenceStat<uint64_t> d_resourceUnitsUsed;
+}; /* struct SmtEngineStatistics */
+
+} // namespace smt
+} // namespace CVC4
+
+#endif /* CVC4__SMT__SMT_ENGINE_STATS_H */
projects / cvc5.git / commitdiff