diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-30 14:12:56 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-30 19:12:56 +0000 |
commit | 327a24508ed1d02a3fa233e680ffd0b30aa685a9 (patch) | |
tree | d130a4b5afcf34383b6bdf38c433d77c5911709d /src/smt/preprocessor.h | |
parent | 38a45651953d3bcfe67cb80b4f2ba2d1b278f7ba (diff) |
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.
Diffstat (limited to 'src/smt/preprocessor.h')
-rw-r--r-- | src/smt/preprocessor.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index c590b7164..e0ad2cc14 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -25,6 +25,7 @@ #include "theory/booleans/circuit_propagator.h" namespace cvc5 { +class Env; namespace preprocessing { class PreprocessingPassContext; } @@ -46,7 +47,7 @@ class Preprocessor { public: Preprocessor(SmtEngine& smt, - context::UserContext* u, + Env& env, AbstractValues& abs, SmtEngineStatistics& stats); ~Preprocessor(); @@ -94,17 +95,16 @@ class Preprocessor const Node& n, std::unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly = false); - /** * Set proof node manager. Enables proofs in this preprocessor. */ void setProofGenerator(PreprocessProofGenerator* pppg); private: - /** A copy of the current context */ - context::Context* d_context; /** Reference to the parent SmtEngine */ SmtEngine& d_smt; + /** Reference to the env */ + Env& d_env; /** Reference to the abstract values utility */ AbstractValues& d_absValues; /** |