diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-21 12:08:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-21 12:08:14 -0500 |
| commit | b8301cde27c455c8da3e9017072a577a0816939b (patch) | |
| tree | 816d1cccdda0625419b1b088644bafb85a857d14 /test | |
| parent | 905dc2b51fd0145e0bb69a166c06a1731ef4c44b (diff) | |
Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930)
This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.
This addresses CVC4/cvc4-projects#113.
Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:
QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.
Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/quantifiers/cegqi-nl-simp.cvc | 1 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue3647.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/nl/sin1-deq-sat.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/nl/sin1-sat.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3648.smt2 | 2 |
5 files changed, 5 insertions, 4 deletions
diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc index d01d7b7d2..eaefbe651 100644 --- a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc +++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc @@ -1,2 +1,3 @@ +% COMMAND-LINE: --nl-rlv=none % EXPECT: entailed QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ; diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2 index 0fc0f55f9..6c66d2e4c 100644 --- a/test/regress/regress1/nl/issue3647.smt2 +++ b/test/regress/regress1/nl/issue3647.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-models --produce-models --decision=internal +; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/regress1/nl/sin1-deq-sat.smt2 b/test/regress/regress1/nl/sin1-deq-sat.smt2 index d9e12c7b4..4fb0732a3 100644 --- a/test/regress/regress1/nl/sin1-deq-sat.smt2 +++ b/test/regress/regress1/nl/sin1-deq-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2 index d2a21fa60..9c1d9cef6 100644 --- a/test/regress/regress1/nl/sin1-sat.smt2 +++ b/test/regress/regress1/nl/sin1-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2 index e7b7547c4..2fc1a6115 100644 --- a/test/regress/regress1/sygus/issue3648.smt2 +++ b/test/regress/regress1/sygus/issue3648.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; COMMAND-LINE: --sygus-inference --no-check-models +; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always (set-logic ALL) (declare-fun a () Real) (assert (> a 0.000001)) |