diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-24 15:02:04 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-24 15:02:04 -0500 |
commit | 3538f6f4700b3fa357e1c767ee6cd42be87a78b8 (patch) | |
tree | cbc571c8a41e7ec330b6679b7f64b2920f1a939f /src/smt | |
parent | 3075a8e20dba6a784316714543c8a1b262459d9a (diff) |
Function definition fmf preprocessing pass (#5064)
This defines the function definition finite model finding as a proper preprocessing pass.
This is required for cleaning/fixing bugs in the preprocessor on proof-new.
There are no intended behavior changes in this PR, although the code for the pass was updated to the new style guidelines.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/process_assertions.cpp | 47 | ||||
-rw-r--r-- | src/smt/process_assertions.h | 6 |
2 files changed, 7 insertions, 46 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 3712d1914..504814e07 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -32,7 +32,6 @@ #include "smt/dump.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; @@ -54,18 +53,13 @@ class ScopeCounter }; ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm) - : d_smt(smt), - d_resourceManager(rm), - d_preprocessingPassContext(nullptr), - d_fmfRecFunctionsDefined(nullptr) + : d_smt(smt), d_resourceManager(rm), d_preprocessingPassContext(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) @@ -140,7 +134,11 @@ bool ProcessAssertions::apply(Assertions& as) unordered_map<Node, Node, NodeHashFunction> cache; for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) { - assertions.replace(i, expandDefinitions(assertions[i], cache)); + Node expd = expandDefinitions(assertions[i], cache); + if (expd != assertions[i]) + { + assertions.replace(i, expd); + } } } Trace("smt-proc") @@ -247,38 +245,7 @@ bool ProcessAssertions::apply(Assertions& as) // 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); - } + d_passes["fun-def-fmf"]->apply(&assertions); } } diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index ba5298abe..a4f16ab1d 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -107,12 +107,6 @@ class ProcessAssertions * 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); /** |