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.

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index d0b0ccb87cb4bb0f563ad22192bfbd92b00ac9c9..91f0b9b6373550bb927567d55bb55cfa9a4caabe 100644 (file)
--- 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<Node> 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<Node> 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<Node, Node> SolverEngine::getSepHeapAndNilExpr(void)
   return std::make_pair(heap, nil);
 }
 
-std::vector<Node> SolverEngine::getAssertionsInternal()
+std::vector<Node> SolverEngine::getAssertionsInternal() const
 {
   Assert(d_state->isFullyInited());
   const CDList<Node>& al = d_asserts->getAssertionList();

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 3b509bf468bb836ad81759b8bba9625ba96e03ae..ca4d763b0c7bd5fd3004096b585bd9dde24f289f 100644 (file)
--- 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<Node> getAssertionsInternal();
+  std::vector<Node> 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 30e901bd12ecef5c42724597f1d0c94561dbb72f..24d311604173f25af100b3e01c012dc98825d855 100644 (file)
--- 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 (file)
index 0000000..4574ec4
--- /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 fca80a9605cc92b6ff54af2f4aae463c3a00650c..f1b6f72bd1f67ba27e8358c00177d4f39a4f3cd1 100644 (file)
--- 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 b16bbdda060a70d0f0b0c2569ae25332bef1b55a..84407241181aacdc2646c821dbb0f9bd09884490 100644 (file)
--- 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 05414230aed7397ca2c1d4c63413d71cc901e614..632fdbf7059c956eb6fa2f2b41c80d2862a74f28 100644 (file)
--- 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 (file)
index 0000000..f85cc96
--- /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 2dd39ec0b45f9284f46d88a63cdb5cdf73ce72df..bcd647cdaedbab1fb2bc75d37e1d806d4d9cd24b 100644 (file)
--- 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 35445e92799f02ed479a359c2d99f22328cf9fb4..ece8372327924538793ffc115396cd7664f03335 100644 (file)
--- 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