From 327a24508ed1d02a3fa233e680ffd0b30aa685a9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 30 Apr 2021 14:12:56 -0500 Subject: Use substitutions for implementing defined functions (#6437) This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions. In other words, the effect of: (define-fun f X t) is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when (= f (lambda X t)) was an equality solved by non-clausal simplification The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula. In this PR: define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline. Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit. The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions. The proof manager does not require a special case of using the define-function maps. Define-function maps are eliminated from SmtEngine. Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR. --- src/smt/process_assertions.cpp | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'src/smt/process_assertions.cpp') diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index fa230cd54..cf747c360 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -31,7 +31,6 @@ #include "preprocessing/preprocessing_pass_registry.h" #include "printer/printer.h" #include "smt/assertions.h" -#include "smt/defined_function.h" #include "smt/dump.h" #include "smt/expand_definitions.h" #include "smt/smt_engine.h" @@ -59,11 +58,9 @@ class ScopeCounter }; ProcessAssertions::ProcessAssertions(SmtEngine& smt, - ExpandDefs& exDefs, ResourceManager& rm, SmtEngineStatistics& stats) : d_smt(smt), - d_exDefs(exDefs), d_resourceManager(rm), d_smtStats(stats), d_preprocessingPassContext(nullptr) @@ -136,11 +133,11 @@ bool ProcessAssertions::apply(Assertions& as) << "ProcessAssertions::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", assertions); - // Expand definitions, which replaces defined functions with their definition - // and does beta reduction. Notice we pass true as the second argument since - // we do not want to call theories to expand definitions here, since we want + // Apply substitutions first. If we are non-incremental, this has only the + // effect of replacing defined functions with their definitions. + // We do not call theory-specific expand definitions here, since we want // to give the opportunity to rewrite/preprocess terms before expansion. - d_exDefs.expandAssertions(assertions, true); + d_passes["apply-substs"]->apply(&assertions); Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-definition-expansion" << endl; -- cgit v1.2.3