fix

kondylidou · Jan 31, 2025 · eb595d1 · eb595d1
1 parent d34e412
commit eb595d1
Show file tree

Hide file tree

Showing 13 changed files with 19 additions and 19 deletions.
diff --git a/NEWS.md b/NEWS.md
@@ -51,7 +51,7 @@ cvc5 1.2.0
   by cvc5. The plugin class also contains a callback for the user to introduce
   new learned clauses into the state of cvc5 during solving.
 
-- Added a new strategy `--mbqi-fast-sygus` (disabled by default) for **quantifier
+- Added a new strategy `--mbqi-enum` (disabled by default) for **quantifier
   instantiation** which uses SyGuS enumeration to augment instantiations from
   model-based quantifier instantiation.
 

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -111,23 +111,23 @@ UFBV)
   trywith 150 --sygus-inst
   trywith 150 --mbqi --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --cegqi-nested-qe --decision=internal
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 30 --enum-inst --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 ABV|BV)
   trywith 80 --enum-inst
   trywith 80 --sygus-inst
   trywith 80 --mbqi --no-cegqi --no-sygus-inst
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --cegqi-nested-qe --decision=internal
   trywith 30 --enum-inst --no-cegqi-bv
   trywith 30 --enum-inst --cegqi-bv-ineq=eq-slack
   # finish 10min
   finishwith --enum-inst --no-cegqi-innermost --global-negate
   ;;
 ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA|BVFPLRA)
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --nl-ext-tplanes
   trywith 60 --mbqi --no-cegqi --no-sygus-inst
   finishwith --sygus-inst
@@ -136,7 +136,7 @@ LIA|LRA)
   trywith 30 --enum-inst
   trywith 300 --enum-inst --cegqi-nested-qe
   trywith 30 --mbqi --no-cegqi --no-sygus-inst
-  trywith 30 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 30 --mbqi-enum --no-cegqi --no-sygus-inst
   finishwith --enum-inst --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2024 b/contrib/competitions/smt-comp/run-script-smtcomp2024
@@ -111,23 +111,23 @@ UFBV)
   trywith 150 --sygus-inst
   trywith 150 --mbqi --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --cegqi-nested-qe --decision=internal
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 30 --enum-inst --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 ABV|BV)
   trywith 80 --enum-inst
   trywith 80 --sygus-inst
   trywith 80 --mbqi --no-cegqi --no-sygus-inst
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --cegqi-nested-qe --decision=internal
   trywith 30 --enum-inst --no-cegqi-bv
   trywith 30 --enum-inst --cegqi-bv-ineq=eq-slack
   # finish 10min
   finishwith --enum-inst --no-cegqi-innermost --global-negate
   ;;
 ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA|BVFPLRA)
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --nl-ext-tplanes
   trywith 60 --mbqi --no-cegqi --no-sygus-inst
   finishwith --sygus-inst
@@ -136,7 +136,7 @@ LIA|LRA)
   trywith 30 --enum-inst
   trywith 300 --enum-inst --cegqi-nested-qe
   trywith 30 --mbqi --no-cegqi --no-sygus-inst
-  trywith 30 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 30 --mbqi-enum --no-cegqi --no-sygus-inst
   finishwith --enum-inst --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
@@ -1436,7 +1436,7 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   {
     SET_AND_NOTIFY(quantifiers, cegqi, false, "instMaxLevel");
   }
-  // enable MBQI if --mbqi-fast-sygus is provided
+  // enable MBQI if --mbqi-enum is provided
   if (opts.quantifiers.mbqiFastSygus)
   {
     SET_AND_NOTIFY_IF_NOT_USER(quantifiers, mbqi, true, "mbqiFastSygus");

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
@@ -181,7 +181,7 @@ void QuantifiersEngine::ppNotifyAssertions(
   }
   if (options().quantifiers.mbqi)
   {
-    // may need to be notified of assertions, for mbqi-fast-sygus
+    // may need to be notified of assertions, for mbqi-enum
     quantifiers::InstStrategyMbqi* mi = d_qmodules->d_mbqi.get();
     mi->ppNotifyAssertions(assertions);
   }

diff --git a/test/regress/cli/regress0/ho/dd.lcl720.smt2 b/test/regress/cli/regress0/ho/dd.lcl720.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: sat
 (set-logic HO_ALL)
 (declare-const P (-> Int Bool))

diff --git a/test/regress/cli/regress0/ho/m-enum-bug1.smt2 b/test/regress/cli/regress0/ho/m-enum-bug1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 (set-logic HO_ALL)
 (declare-sort a 0)

diff --git a/test/regress/cli/regress0/ho/m-enum-bug2.smt2 b/test/regress/cli/regress0/ho/m-enum-bug2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 (set-logic HO_ALL)
 (declare-sort a 0)

diff --git a/test/regress/cli/regress0/ho/m-enum-bug3.smt2 b/test/regress/cli/regress0/ho/m-enum-bug3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 (set-logic HO_ALL)
 (declare-sort a 0)

diff --git a/test/regress/cli/regress1/quantifiers/ho-grammar.smt2 b/test/regress/cli/regress1/quantifiers/ho-grammar.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 (set-logic HO_ALL)

diff --git a/test/regress/cli/regress1/quantifiers/lcl579-2-ho-mbqi.smt2 b/test/regress/cli/regress1/quantifiers/lcl579-2-ho-mbqi.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 (set-logic HO_ALL)
 (declare-sort a 0)

diff --git a/test/regress/cli/regress1/quantifiers/mbqi_fast_sy_check_ic.smt2 b/test/regress/cli/regress1/quantifiers/mbqi_fast_sy_check_ic.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi-fast-sygus --no-cegqi
+; COMMAND-LINE: --mbqi-enum --no-cegqi
 ; EXPECT: unsat
 (set-logic BV)
 (declare-fun t () (_ BitVec 4))

diff --git a/test/regress/cli/regress1/seq/proj-issue733-mbqi-w.smt2 b/test/regress/cli/regress1/seq/proj-issue733-mbqi-w.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic ALL)
-(set-option :mbqi-fast-sygus true)
+(set-option :mbqi-enum true)
 (declare-const x (Seq Bool))
 (assert (distinct (seq.at x 9510904) (seq.++ (seq.at x 9510904) (seq.rev (seq.at x 9510904)))))
 (check-sat)