From 4cf79c69a6c6ef8bb26f0119e85450a3cf7028a3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Feb 2022 12:46:02 -0600 Subject: [PATCH] Option exception when incompatible with proofs (#8064) This changes set defaults so that it doesn't silently disable proofs or unsat cores. Fixes cvc5/cvc5-projects#440. --- src/smt/set_defaults.cpp | 10 +++------- test/regress/regress0/quantifiers/lra-triv-gn.smt2 | 4 +++- test/regress/regress1/issue3970-nl-ext-purify.smt2 | 2 ++ .../regress1/quantifiers/issue4021-ind-opts.smt2 | 3 ++- test/regress/regress1/sygus/issue3201.smt2 | 2 ++ test/regress/regress1/sygus/issue3247.smt2 | 2 ++ .../regress1/sygus/issue3995-fmf-var-op.smt2 | 2 ++ test/regress/regress1/sygus/issue4009-qep.smt2 | 2 ++ .../regress1/sygus/issue4025-no-rlv-cond.smt2 | 2 ++ .../regress1/sygus/issue4083-var-shadow.smt2 | 2 ++ test/regress/regress1/sygus/proj-issue185.smt2 | 2 ++ test/unit/api/cpp/solver_black.cpp | 13 +++++++++++++ 12 files changed, 37 insertions(+), 9 deletions(-) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 5a7181f7b..e444ea275 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -169,13 +169,9 @@ void SetDefaults::setDefaultsPre(Options& opts) std::stringstream reasonNoProofs; if (incompatibleWithProofs(opts, reasonNoProofs)) { - opts.smt.unsatCores = false; - opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; - notifyModifyOption( - "produceProofs and unsatCores", "false", reasonNoProofs.str()); - opts.smt.produceProofs = false; - opts.smt.checkProofs = false; - opts.smt.proofMode = options::ProofMode::OFF; + std::stringstream ss; + ss << reasonNoProofs.str() << " not supported with proofs or unsat cores"; + throw OptionException(ss.str()); } } if (d_isInternalSubsolver) diff --git a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/regress0/quantifiers/lra-triv-gn.smt2 index 7cc9c2ea3..0d36d2037 100644 --- a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 +++ b/test/regress/regress0/quantifiers/lra-triv-gn.smt2 @@ -1,5 +1,7 @@ -; COMMAND-LINE: --global-negate --no-check-unsat-cores +; COMMAND-LINE: --global-negate ; EXPECT: unsat +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic LRA) (set-info :status unsat) (assert (not (exists ((?X Real)) (>= (/ (- 13) 4) ?X)))) diff --git a/test/regress/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/regress1/issue3970-nl-ext-purify.smt2 index c19884a63..a48660bd8 100644 --- a/test/regress/regress1/issue3970-nl-ext-purify.smt2 +++ b/test/regress/regress1/issue3970-nl-ext-purify.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: unsat +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic QF_UFNRA) (set-option :nl-ext-purify true) (set-option :sygus-inference true) diff --git a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 index 9cb5cdac3..beafff29b 100644 --- a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 +++ b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic HO_ALL) (set-option :ag-miniscope-quant true) (set-option :conjecture-gen true) diff --git a/test/regress/regress1/sygus/issue3201.smt2 b/test/regress/regress1/sygus/issue3201.smt2 index f9df0e782..212fca782 100644 --- a/test/regress/regress1/sygus/issue3201.smt2 +++ b/test/regress/regress1/sygus/issue3201.smt2 @@ -1,5 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-inference -q +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic ALL) (declare-fun v () Bool) (assert false) diff --git a/test/regress/regress1/sygus/issue3247.smt2 b/test/regress/regress1/sygus/issue3247.smt2 index a02fbc5ce..7e2f439ce 100644 --- a/test/regress/regress1/sygus/issue3247.smt2 +++ b/test/regress/regress1/sygus/issue3247.smt2 @@ -1,5 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-inference --strings-exp -q +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic ALL) (declare-fun a () String) (declare-fun b () String) diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 index 711afb2d8..48b4ab38c 100644 --- a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 +++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 @@ -1,5 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-inference --fmf-bound +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic HO_ALL) (declare-fun a () (_ BitVec 1)) (assert (bvsgt (bvsmod a a) #b0)) diff --git a/test/regress/regress1/sygus/issue4009-qep.smt2 b/test/regress/regress1/sygus/issue4009-qep.smt2 index 71b9f20bd..67007bac2 100644 --- a/test/regress/regress1/sygus/issue4009-qep.smt2 +++ b/test/regress/regress1/sygus/issue4009-qep.smt2 @@ -1,5 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-inference --sygus-qe-preproc -q +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic ALL) (declare-fun a () Real) (declare-fun b () Real) diff --git a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 index cc0c329cd..426316be4 100644 --- a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 +++ b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 @@ -1,3 +1,5 @@ +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic ALL) (set-option :sygus-inference true) (set-option :sygus-simple-sym-break none) diff --git a/test/regress/regress1/sygus/issue4083-var-shadow.smt2 b/test/regress/regress1/sygus/issue4083-var-shadow.smt2 index 91b77bfaa..0afc35e00 100644 --- a/test/regress/regress1/sygus/issue4083-var-shadow.smt2 +++ b/test/regress/regress1/sygus/issue4083-var-shadow.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: unsat +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic ALL) (set-option :miniscope-quant true) (set-option :sygus-inference true) diff --git a/test/regress/regress1/sygus/proj-issue185.smt2 b/test/regress/regress1/sygus/proj-issue185.smt2 index a3e4b8205..141ab0ae0 100644 --- a/test/regress/regress1/sygus/proj-issue185.smt2 +++ b/test/regress/regress1/sygus/proj-issue185.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: unsat +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof (set-logic ALL) (set-option :sygus-inference true) (set-info :status unsat) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 124a68ead..c6a303c8f 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -3003,6 +3003,19 @@ TEST_F(TestApiBlackSolver, proj_issue414) ASSERT_NO_THROW(slv.simplify(t54)); } +TEST_F(TestApiBlackSolver, proj_issue440) +{ + Solver slv; + slv.setLogic("QF_ALL"); + slv.setOption("global-negate", "true"); + slv.setOption("produce-unsat-cores", "true"); + Sort s1 = slv.getBooleanSort(); + Term t9 = slv.mkBoolean(true); + Term t109 = slv.mkTerm(Kind::NOT, {t9}); + // should throw an option exception + ASSERT_THROW(slv.checkSatAssuming({t109}), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, proj_issue434) { Solver slv; -- 2.30.2