From: Andrew Reynolds Date: Thu, 9 Apr 2020 01:26:11 +0000 (-0500) Subject: Split ProcessAssertions module from SmtEngine (#4210) X-Git-Tag: cvc5-1.0.0~3393 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f8caabd570dd5bb2936d9f094b7b302a510aa6d;p=cvc5.git Split ProcessAssertions module from SmtEngine (#4210) 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. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 447ca90f8..dec5a7f16 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -223,6 +223,7 @@ libcvc4_add_sources( 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 @@ -236,12 +237,16 @@ libcvc4_add_sources( 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 diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 1c0351bcb..4865ccead 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -149,7 +149,6 @@ header = "options/arith_options.h" 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]] diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h new file mode 100644 index 000000000..b141ef9cb --- /dev/null +++ b/src/smt/defined_function.h @@ -0,0 +1,60 @@ +/********************* */ +/*! \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 + +#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& 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& 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 d_formals; + /** the formula */ + Node d_formula; +}; /* class DefinedFunction */ + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__DEFINED_FUNCTION_H */ diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp new file mode 100644 index 000000000..0e2701a1a --- /dev/null +++ b/src/smt/process_assertions.cpp @@ -0,0 +1,871 @@ +/********************* */ +/*! \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 +#include + +#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 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 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::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>::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 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 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 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& cache, + bool expandOnly) +{ + NodeManager* nm = d_smt.d_nodeManager; + std::stack> worklist; + std::stack 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::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 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(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& skolemSet, + unordered_map& cache) +{ + unordered_map::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& cache) +{ + unordered_map::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 diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h new file mode 100644 index 000000000..ddf5a6cba --- /dev/null +++ b/src/smt/process_assertions.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \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 + +#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 NodeList; + typedef unordered_map NodeToNodeHashMap; + typedef unordered_map 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> + d_passes; + /** + * Number of calls of simplify assertions active. + */ + unsigned d_simplifyAssertionsDepth; + /** recursive function definition abstractions for fmf-fun */ + std::map d_fmfRecFunctionsAbs; + /** map to concrete definitions for fmf-fun */ + std::map> 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& 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 diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index d1eed0748..a0f1b2715 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -140,6 +140,29 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) 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(); @@ -772,6 +795,8 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) options::ufssFairnessMonotone.set(false); options::quantEpr.set(false); options::globalNegate.set(false); + options::bvAbstraction.set(false); + options::arithMLTrick.set(false); } if (logic.hasCardinalityConstraints()) { @@ -1405,6 +1430,17 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index dee3365fb..240533fba 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -82,12 +82,15 @@ #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" @@ -143,122 +146,6 @@ void DeleteAndClearCommandVector(std::vector& commands) { 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 d_formals; - Node d_formula; -public: - DefinedFunction() {} - DefinedFunction(Node func, vector& formals, Node formula) - : d_func(func), d_formals(formals), d_formula(formula) - { - } - Node getFunction() const { return d_func; } - vector 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 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) {} @@ -442,13 +329,15 @@ class SmtEnginePrivate : public NodeManagerListener { */ 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 d_preprocessingPassContext; + + /** Process assertions module */ + ProcessAssertions d_processor; + //------------------------------- expression names /** mapping from expressions to name */ context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames; @@ -480,39 +369,10 @@ class SmtEnginePrivate : public NodeManagerListener { CDO d_sygusConjectureStale; /*------------------- end of sygus utils ------------------*/ - private: - std::unique_ptr d_preprocessingPassContext; - - /** - * Map of preprocessing pass instances, mapping from names to preprocessing - * pass instance - */ - std::unordered_map> d_passes; - - /** - * Helper function to fix up assertion list to restore invariants needed after - * ite removal. - */ - void collectSkolems(TNode n, set& 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(), @@ -523,7 +383,7 @@ class SmtEnginePrivate : public NodeManagerListener { 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()), @@ -531,7 +391,6 @@ class SmtEnginePrivate : public NodeManagerListener { { 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))); @@ -607,8 +466,6 @@ class SmtEnginePrivate : public NodeManagerListener { d_smt.d_nodeManager->unsubscribeEvents(this); } - void cleanupPreprocessingPasses() { d_passes.clear(); } - ResourceManager* getResourceManager() { return d_resourceManager; } void spendResource(ResourceManager::Resource r) @@ -616,6 +473,8 @@ class SmtEnginePrivate : public NodeManagerListener { d_resourceManager->spendResource(r); } + ProcessAssertions* getProcessAssertions() { return &d_processor; } + void nmNotifyNewSort(TypeNode tn, uint32_t flags) override { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), @@ -724,12 +583,6 @@ class SmtEnginePrivate : public NodeManagerListener { 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. @@ -738,7 +591,7 @@ class SmtEnginePrivate : public NodeManagerListener { // 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(); @@ -804,7 +657,6 @@ SmtEngine::SmtEngine(ExprManager* em) d_proofManager(nullptr), d_rewriter(new theory::Rewriter()), d_definedFunctions(nullptr), - d_fmfRecFunctionsDefined(nullptr), d_assertionList(nullptr), d_assignments(nullptr), d_modelGlobalCommands(), @@ -847,7 +699,6 @@ SmtEngine::SmtEngine(ExprManager* em) #endif d_definedFunctions = new (true) DefinedFunctionMap(getUserContext()); - d_fmfRecFunctionsDefined = new (true) NodeList(getUserContext()); d_modelCommands = new (true) smt::CommandList(getUserContext()); } @@ -1011,10 +862,9 @@ SmtEngine::~SmtEngine() } 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 @@ -1437,319 +1287,11 @@ bool SmtEngine::isDefinedFunction( Expr func ){ 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 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& cache, bool expandOnly) -{ - stack> worklist; - stack 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::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 formals; - TNode fm; - if( n.getOperator().getKind() == kind::LAMBDA ){ - TNode op = n.getOperator(); - // lambda - for( unsigned i=0; ifind(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(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() { @@ -1835,93 +1377,16 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const return m; } -void SmtEnginePrivate::collectSkolems(TNode n, set& skolemSet, unordered_map& cache) -{ - unordered_map::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& cache) -{ - unordered_map::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. @@ -1933,334 +1398,8 @@ void SmtEnginePrivate::processAssertions() { 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(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 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::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; jsecond.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; ipush_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 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 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 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(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() ); @@ -2269,16 +1408,12 @@ void SmtEnginePrivate::processAssertions() { 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()) { @@ -2917,7 +2052,8 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) } unordered_map 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(); @@ -2949,7 +2085,7 @@ Expr SmtEngine::getValue(const Expr& ex) const // Expand, then normalize unordered_map 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 @@ -3073,7 +2209,7 @@ vector> SmtEngine::getAssignment() // Expand, then normalize unordered_map 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; @@ -3239,7 +2375,7 @@ std::vector SmtEngine::getExpandedAssertions() 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; @@ -3481,7 +2617,7 @@ void SmtEngine::checkModel(bool hardFailure) { // Apply any define-funs from the problem. { unordered_map cache; - n = d_private->expandDefinitions(n, cache); + n = d_private->getProcessAssertions()->expandDefinitions(n, cache); } Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl; @@ -3635,7 +2771,8 @@ void SmtEngine::checkSynthSolution() 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"; @@ -3952,7 +3089,7 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) Node conjn = Node::fromExpr(conj); // must expand definitions std::unordered_map cache; - conjn = d_private->expandDefinitions(conjn, cache); + conjn = d_private->getProcessAssertions()->expandDefinitions(conjn, cache); // now negate conjn = conjn.negate(); d_abdConj = conjn.toExpr(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3f24c8bab..672bec821 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -96,7 +96,7 @@ namespace smt { struct SmtEngineStatistics; class SmtEnginePrivate; class SmtScope; - class BooleanTermConverter; + class ProcessAssertions; ProofManager* currentProofManager(); @@ -130,7 +130,7 @@ class CVC4_PUBLIC SmtEngine 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 @@ -1131,11 +1131,6 @@ class CVC4_PUBLIC SmtEngine */ Expr d_abdConj; - /** recursive function definition abstractions for --fmf-fun */ - std::map d_fmfRecFunctionsAbs; - std::map > d_fmfRecFunctionsConcrete; - NodeList* d_fmfRecFunctionsDefined; - /** * The assertion list (before any conversion) for supporting * getAssertions(). Only maintained if in interactive mode. diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp new file mode 100644 index 000000000..c45f77b9b --- /dev/null +++ b/src/smt/smt_engine_stats.cpp @@ -0,0 +1,73 @@ +/********************* */ +/*! \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 diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h new file mode 100644 index 000000000..cebf85d95 --- /dev/null +++ b/src/smt/smt_engine_stats.h @@ -0,0 +1,63 @@ +/********************* */ +/*! \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 d_resourceUnitsUsed; +}; /* struct SmtEngineStatistics */ + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__SMT_ENGINE_STATS_H */