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 /test/regress | |
| 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 'test/regress')
4 files changed, 5 insertions, 4 deletions
diff --git a/test/regress/regress1/bug516.smt2 b/test/regress/regress1/bug516.smt2 index a01eb97e9..43d18575e 100644 --- a/test/regress/regress1/bug516.smt2 +++ b/test/regress/regress1/bug516.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-bound-int +; COMMAND-LINE: --finite-model-find --fmf-bound-int -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/model-blocker-values.smt2 b/test/regress/regress1/model-blocker-values.smt2 index 65db79ca4..1c9e80642 100644 --- a/test/regress/regress1/model-blocker-values.smt2 +++ b/test/regress/regress1/model-blocker-values.smt2 @@ -1,7 +1,8 @@ ; COMMAND-LINE: --incremental --produce-models --block-models=values ; EXPECT: sat ; EXPECT: sat -; EXPECT: sat +; if we only block models restricted to (a,b), then there are only 2 models +; EXPECT: unsat (set-logic QF_UFLIA) (declare-fun a () Int) (declare-fun b () Int) diff --git a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 index fdbac9996..585ea0602 100644 --- a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 +++ b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv +; COMMAND-LINE: --cegqi-bv -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/issue3664.smt2 b/test/regress/regress1/quantifiers/issue3664.smt2 index 28e999604..e1a923f98 100644 --- a/test/regress/regress1/quantifiers/issue3664.smt2 +++ b/test/regress/regress1/quantifiers/issue3664.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun-rlv --sygus-inference +; COMMAND-LINE: --fmf-fun-rlv --sygus-inference --no-check-models ; EXPECT: sat (set-logic QF_NRA) (declare-fun a () Real) |