Update default options for sygus (#2586)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index e8d8fbe3d0c23960a8a4deda1e22a9b042aa8f1c..eb32beef5f0047e55aaca2412a3170c172e52831 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1021,7 +1021,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-repair-const"
   type       = "bool"
-  default    = "true"
+  default    = "false"
   help       = "use approach to repair constants in sygus candidate solutions"
 
 [[option]]

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 11c03de6cbf4ed2a9ad13372aa1e07dc1299733a..3348799933c2dee78a6376ede172b7a4430e88da 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1634,35 +1634,40 @@ void SmtEngine::setDefaults() {
   // Set decision mode based on logic (if not set by user)
   if(!options::decisionMode.wasSetByUser()) {
     decision::DecisionMode decMode =
-      // ALL
-      d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION :
-      ( // QF_BV
-        (not d_logic.isQuantified() &&
-          d_logic.isPure(THEORY_BV)
-          ) ||
-        // QF_AUFBV or QF_ABV or QF_UFBV
-        (not d_logic.isQuantified() &&
-         (d_logic.isTheoryEnabled(THEORY_ARRAYS) ||
-          d_logic.isTheoryEnabled(THEORY_UF)) &&
-         d_logic.isTheoryEnabled(THEORY_BV)
-         ) ||
-        // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
-        (not d_logic.isQuantified() &&
-         d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
-         d_logic.isTheoryEnabled(THEORY_UF) &&
-         d_logic.isTheoryEnabled(THEORY_ARITH)
-         ) ||
-        // QF_LRA
-        (not d_logic.isQuantified() &&
-         d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
-         ) ||
-        // Quantifiers
-        d_logic.isQuantified() ||
-        // Strings
-        d_logic.isTheoryEnabled(THEORY_STRINGS)
-        ? decision::DECISION_STRATEGY_JUSTIFICATION
-        : decision::DECISION_STRATEGY_INTERNAL
-      );
+        // sygus uses internal
+        is_sygus ? decision::DECISION_STRATEGY_INTERNAL :
+                 // ALL
+            d_logic.hasEverything()
+                ? decision::DECISION_STRATEGY_JUSTIFICATION
+                : (  // QF_BV
+                      (not d_logic.isQuantified() && d_logic.isPure(THEORY_BV))
+                              ||
+                              // QF_AUFBV or QF_ABV or QF_UFBV
+                              (not d_logic.isQuantified()
+                               && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
+                                   || d_logic.isTheoryEnabled(THEORY_UF))
+                               && d_logic.isTheoryEnabled(THEORY_BV))
+                              ||
+                              // QF_AUFLIA (and may be ends up enabling
+                              // QF_AUFLRA?)
+                              (not d_logic.isQuantified()
+                               && d_logic.isTheoryEnabled(THEORY_ARRAYS)
+                               && d_logic.isTheoryEnabled(THEORY_UF)
+                               && d_logic.isTheoryEnabled(THEORY_ARITH))
+                              ||
+                              // QF_LRA
+                              (not d_logic.isQuantified()
+                               && d_logic.isPure(THEORY_ARITH)
+                               && d_logic.isLinear()
+                               && !d_logic.isDifferenceLogic()
+                               && !d_logic.areIntegersUsed())
+                              ||
+                              // Quantifiers
+                              d_logic.isQuantified() ||
+                              // Strings
+                              d_logic.isTheoryEnabled(THEORY_STRINGS)
+                          ? decision::DECISION_STRATEGY_JUSTIFICATION
+                          : decision::DECISION_STRATEGY_INTERNAL);
 
     bool stoponly =
       // ALL
@@ -1895,13 +1900,11 @@ void SmtEngine::setDefaults() {
   //counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
   if (d_logic.isQuantified()
-      && ((options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL
-           && (d_logic.isTheoryEnabled(THEORY_ARITH)
-               || d_logic.isTheoryEnabled(THEORY_DATATYPES)
-               || d_logic.isTheoryEnabled(THEORY_BV)
-               || d_logic.isTheoryEnabled(THEORY_FP)))
-          || d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)
-          || options::cbqiAll()))
+          && (d_logic.isTheoryEnabled(THEORY_ARITH)
+              || d_logic.isTheoryEnabled(THEORY_DATATYPES)
+              || d_logic.isTheoryEnabled(THEORY_BV)
+              || d_logic.isTheoryEnabled(THEORY_FP))
+      || options::cbqiAll())
   {
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
@@ -1942,8 +1945,7 @@ void SmtEngine::setDefaults() {
       options::cbqiNestedQE.set(false);
     }
     // prenexing
-    if (options::cbqiNestedQE()
-        || options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL)
+    if (options::cbqiNestedQE())
     {
       // only complete with prenex = disj_normal or normal
       if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL)

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 0db05d93c6a5c7c82bbe5de8d460f115e0f0754b..7d3947bf4cc3b25712c79d3939ba6abb91576751 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1033,7 +1033,7 @@ Node SygusSymBreakNew::registerSearchValue(Node a,
     Node bv = d_tds->sygusToBuiltin(cnv, tn);
     Trace("sygus-sb-debug") << "  ......builtin is " << bv << std::endl;
     Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv);
-    Trace("sygus-sb-debug") << "  ......rewrites to " << bvr << std::endl;
+    Trace("sygus-sb-debug") << "  ......search value rewrites to " << bvr << std::endl;
     Trace("dt-sygus") << "  * DT builtin : " << n << " -> " << bvr << std::endl;
     unsigned sz = d_tds->getSygusTermSize( nv );      
     if( d_tds->involvesDivByZero( bvr ) ){

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 889f4d9c9a92a69e05a49eb39e9278a1a8b4c0d1..8050e97f8970d2159839ec1a18d5a2a1c752db0d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -364,12 +364,12 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
     // are not passive
     return Node::null();
   }
-  e = d_tds->getSynthFunForEnumerator(e);
+  Node ee = d_tds->getSynthFunForEnumerator(e);
   Assert(!e.isNull());
-  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+  std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee);
   if (itx == d_examples_invalid.end()) {
-    unsigned nex = d_examples[e].size();
-    Node ret = d_pbe_trie[e][tn].addPbeExample(tn, e, bvr, this, 0, nex);
+    unsigned nex = d_examples[ee].size();
+    Node ret = d_pbe_trie[e][tn].addPbeExample(tn, ee, bvr, this, 0, nex);
     Assert(ret.getType() == bvr.getType());
     return ret;
   }

diff --git a/test/regress/regress0/sygus/check-generic-red.sy b/test/regress/regress0/sygus/check-generic-red.sy
index 917c1473a4ba86e453aab4ce651fa121e8a898ec..e169e1a5ccb00e4ae83b0199d59b2b6e36c0f06a 100644 (file)
--- a/test/regress/regress0/sygus/check-generic-red.sy
+++ b/test/regress/regress0/sygus/check-generic-red.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification
 (set-logic LIA)
 
 (synth-fun P ((x Int) (y Int)) Bool

diff --git a/test/regress/regress1/sygus/array_search_5-Q-easy.sy b/test/regress/regress1/sygus/array_search_5-Q-easy.sy
index e1f37d2cd95116e7f01e31cc0cb130b548842398..8be52a5775ad0e8ca171553d32a218fd9557e29d 100644 (file)
--- a/test/regress/regress1/sygus/array_search_5-Q-easy.sy
+++ b/test/regress/regress1/sygus/array_search_5-Q-easy.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification
 ( set-logic LIA )
 ( synth-fun findIdx  (         ( y1  Int )  ( y2  Int )  ( y3  Int )  ( y4  Int )  ( y5  Int )  ( k1  Int ) )  Int (
   (Start  Int (    NT1

diff --git a/test/regress/regress1/sygus/car_3.lus.sy b/test/regress/regress1/sygus/car_3.lus.sy
index b572622f78cb0c7c02f2db0b652f84d51a460b84..088613f218dec51874b58251fa7ea657bb9e0c1d 100755 (executable)
--- a/test/regress/regress1/sygus/car_3.lus.sy
+++ b/test/regress/regress1/sygus/car_3.lus.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-unif --sygus-unif-cond-independent --sygus-unif-boolean-heuristic-dt
+; COMMAND-LINE: --sygus-out=status --sygus-unif --sygus-unif-cond-independent --sygus-unif-boolean-heuristic-dt --decision=justification
 
 (set-logic LIA)
 

diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy
index 43fd7c1ac17bfe731a309a81ae10b953996d77e5..65b17605d2ef9f1cbbf6f8c5e6c2851802bab523 100644 (file)
--- a/test/regress/regress1/sygus/clock-inc-tuple.sy
+++ b/test/regress/regress1/sygus/clock-inc-tuple.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification
 
 (set-logic ALL_SUPPORTED)
 (declare-var m Int)

diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy
index ae8d0b8c0b805129fd34ce3ddb054652f4dc77e4..7b96a2bf32bd997c6d5078b95ecea4dea39889a9 100644 (file)
--- a/test/regress/regress1/sygus/commutative-stream.sy
+++ b/test/regress/regress1/sygus/commutative-stream.sy
@@ -3,7 +3,7 @@
 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; EXIT: 1
 
-; COMMAND-LINE: --sygus-stream --sygus-abort-size=2
+; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 --decision=justification
 
 (set-logic LIA)
 

diff --git a/test/regress/regress1/sygus/logiccell_help.sy b/test/regress/regress1/sygus/logiccell_help.sy
index 34f21ba558cc3b27a613ffcc4783bb420e6b1726..1ba05e64844deff8879b8b1b9c46df6a9df6c9be 100644 (file)
--- a/test/regress/regress1/sygus/logiccell_help.sy
+++ b/test/regress/regress1/sygus/logiccell_help.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --sygus-repair-const
 (set-logic BV)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

diff --git a/test/regress/regress1/sygus/sygus-dt.sy b/test/regress/regress1/sygus/sygus-dt.sy
index d496e3fdca7824d2b5edc2dc7cf1ba2bc556c051..2f3f4dbb9fb08729514490108f5176f21739379a 100644 (file)
--- a/test/regress/regress1/sygus/sygus-dt.sy
+++ b/test/regress/regress1/sygus/sygus-dt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --decision=justification
 
 (set-logic LIA)