From 34f343d6d5783f5df22a360b31c5cd0e9207e637 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 19 May 2022 12:09:09 -0500 Subject: [PATCH] Add options and regressions to increase coverage (#8803) Also corrects an issue with the text interface. When get-model is used with model cores, we do not currently filter the output. This ensures that we do. --- src/smt/solver_engine.cpp | 28 ++++++++++--------- src/smt/solver_engine.h | 2 +- test/regress/cli/CMakeLists.txt | 2 ++ .../cli/regress0/model-core-non-implied.smt2 | 17 +++++++++++ test/regress/cli/regress0/model-core.smt2 | 7 ++++- .../cli/regress1/push-pop/arith_lra_01.smt2 | 2 +- .../cli/regress1/push-pop/fuzz_5_1.smt2 | 2 +- .../cli/regress1/sygus/grammar_norm.sy | 20 +++++++++++++ .../regress2/arith/sc-7.base.cvc.smtv1.smt2 | 2 ++ test/regress/cli/regress2/sygus/qgu-bools.sy | 2 ++ 10 files changed, 67 insertions(+), 17 deletions(-) create mode 100644 test/regress/cli/regress0/model-core-non-implied.smt2 create mode 100644 test/regress/cli/regress1/sygus/grammar_norm.sy diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index d0b0ccb87..91f0b9b63 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -674,6 +674,20 @@ TheoryModel* SolverEngine::getAvailableModel(const char* c) const "check-sat was interrupted?"; throw RecoverableModalException(ss.str().c_str()); } + // compute the model core if necessary and not done so already + const Options& opts = d_env->getOptions(); + if (opts.smt.modelCoresMode != options::ModelCoresMode::NONE + && !m->isUsingModelCore()) + { + // If we enabled model cores, we compute a model core for m based on our + // (expanded) assertions using the model core builder utility. Notice that + // we get the assertions using the getAssertionsInternal, which does not + // impact whether we are in "sat" mode + std::vector asserts = getAssertionsInternal(); + d_smtSolver->getPreprocessor()->expandDefinitions(asserts); + ModelCoreBuilder mcb(*d_env.get()); + mcb.setModelCore(asserts, m, opts.smt.modelCoresMode); + } return m; } @@ -1092,18 +1106,6 @@ bool SolverEngine::isModelCoreSymbol(Node n) return true; } TheoryModel* tm = getAvailableModel("isModelCoreSymbol"); - // compute the model core if not done so already - if (!tm->isUsingModelCore()) - { - // If we enabled model cores, we compute a model core for m based on our - // (expanded) assertions using the model core builder utility. Notice that - // we get the assertions using the getAssertionsInternal, which does not - // impact whether we are in "sat" mode - std::vector asserts = getAssertionsInternal(); - d_smtSolver->getPreprocessor()->expandDefinitions(asserts); - ModelCoreBuilder mcb(*d_env.get()); - mcb.setModelCore(asserts, tm, opts.smt.modelCoresMode); - } return tm->isModelCoreSymbol(n); } @@ -1214,7 +1216,7 @@ std::pair SolverEngine::getSepHeapAndNilExpr(void) return std::make_pair(heap, nil); } -std::vector SolverEngine::getAssertionsInternal() +std::vector SolverEngine::getAssertionsInternal() const { Assert(d_state->isFullyInited()); const CDList& al = d_asserts->getAssertionList(); diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 3b509bf46..ca4d763b0 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -1038,7 +1038,7 @@ class CVC5_EXPORT SolverEngine * or getExpandedAssertions, which may trigger initialization and SMT state * changes. */ - std::vector getAssertionsInternal(); + std::vector getAssertionsInternal() const; /** * Return a reference to options like for `EnvObj`. diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 30e901bd1..24d311604 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -775,6 +775,7 @@ set(regress_0_tests regress0/logops.04.cvc.smt2 regress0/logops.05.cvc.smt2 regress0/model-core.smt2 + regress0/model-core-non-implied.smt2 regress0/models-print-1.smt2 regress0/models-print-2.smt2 regress0/named-expr-use.smt2 @@ -2718,6 +2719,7 @@ set(regress_1_tests regress1/sygus/fg_polynomial3.sy regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy regress1/sygus/find_sc_bvult_bvnot.sy + regress1/sygus/grammar_norm.sy regress1/sygus/ground-ite-free-constant-si.sy regress1/sygus/hd-01-d1-prog.sy regress1/sygus/hd-19-d1-prog-dup-op.sy diff --git a/test/regress/cli/regress0/model-core-non-implied.smt2 b/test/regress/cli/regress0/model-core-non-implied.smt2 new file mode 100644 index 000000000..4574ec41f --- /dev/null +++ b/test/regress/cli/regress0/model-core-non-implied.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --produce-models --model-cores=non-implied +; SCRUBBER: sed 's/(define-fun.*/define-fun/g' +; EXPECT: sat +; EXPECT: ( +; EXPECT: define-fun +; EXPECT: ) +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun w () Int) +(declare-fun u () Int) +(declare-fun v () Int) +(assert (and (= x y) (= y z) (= y w) (= (+ u 1) w))) +; a single value for a variable implies the others +(check-sat) +(get-model) diff --git a/test/regress/cli/regress0/model-core.smt2 b/test/regress/cli/regress0/model-core.smt2 index fca80a960..f1b6f72bd 100644 --- a/test/regress/cli/regress0/model-core.smt2 +++ b/test/regress/cli/regress0/model-core.smt2 @@ -1,6 +1,10 @@ ; COMMAND-LINE: --produce-models --model-cores=simple -; COMMAND-LINE: --produce-models --model-core=non-implied +; SCRUBBER: sed 's/(define-fun.*/define-fun/g' ; EXPECT: sat +; EXPECT: ( +; EXPECT: define-fun +; EXPECT: define-fun +; EXPECT: ) (set-logic QF_UFLIA) (declare-fun x () Int) (declare-fun y () Int) @@ -9,3 +13,4 @@ (assert (= (f x) 0)) (assert (or (> z 5) (> y 5))) (check-sat) +(get-model) diff --git a/test/regress/cli/regress1/push-pop/arith_lra_01.smt2 b/test/regress/cli/regress1/push-pop/arith_lra_01.smt2 index b16bbdda0..844072411 100644 --- a/test/regress/cli/regress1/push-pop/arith_lra_01.smt2 +++ b/test/regress/cli/regress1/push-pop/arith_lra_01.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental +; COMMAND-LINE: --incremental --use-soi ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat diff --git a/test/regress/cli/regress1/push-pop/fuzz_5_1.smt2 b/test/regress/cli/regress1/push-pop/fuzz_5_1.smt2 index 05414230a..632fdbf70 100644 --- a/test/regress/cli/regress1/push-pop/fuzz_5_1.smt2 +++ b/test/regress/cli/regress1/push-pop/fuzz_5_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental +; COMMAND-LINE: --incremental --use-soi ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat diff --git a/test/regress/cli/regress1/sygus/grammar_norm.sy b/test/regress/cli/regress1/sygus/grammar_norm.sy new file mode 100644 index 000000000..f85cc9657 --- /dev/null +++ b/test/regress/cli/regress1/sygus/grammar_norm.sy @@ -0,0 +1,20 @@ +; EXPECT: feasible +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-grammar-norm +(set-logic LIA) + +(synth-fun f ((x Int)) Int + ((Start Int) (StartBool Bool)) + ((Start Int (0 1 x + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (not StartBool) + (<= Start Start))))) + +(declare-var x Int) + +(constraint (= (f x) (* 2 x))) + +(check-synth) diff --git a/test/regress/cli/regress2/arith/sc-7.base.cvc.smtv1.smt2 b/test/regress/cli/regress2/arith/sc-7.base.cvc.smtv1.smt2 index 2dd39ec0b..bcd647cda 100644 --- a/test/regress/cli/regress2/arith/sc-7.base.cvc.smtv1.smt2 +++ b/test/regress/cli/regress2/arith/sc-7.base.cvc.smtv1.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --use-soi +; EXPECT: unsat (set-option :incremental false) (set-info :source "Fully parameterized specification and verification of a synchronizer circuit modeling metastability at various levels of refinement. diff --git a/test/regress/cli/regress2/sygus/qgu-bools.sy b/test/regress/cli/regress2/sygus/qgu-bools.sy index 35445e927..ece837232 100644 --- a/test/regress/cli/regress2/sygus/qgu-bools.sy +++ b/test/regress/cli/regress2/sygus/qgu-bools.sy @@ -1,4 +1,6 @@ ; COMMAND-LINE: --sygus-query-gen=unsat --sygus-abort-size=2 +; COMMAND-LINE: --sygus-query-gen=sample-sat --sygus-abort-size=2 +; COMMAND-LINE: --sygus-query-gen=basic --sygus-abort-size=2 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(query)' ; EXIT: 1 -- 2.30.2