summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options.toml2
-rw-r--r--src/smt/smt_engine.cpp78
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp2
-rw-r--r--src/theory/quantifiers/sygus/sygus_pbe.cpp8
-rw-r--r--test/regress/regress0/sygus/check-generic-red.sy2
-rw-r--r--test/regress/regress1/sygus/array_search_5-Q-easy.sy2
-rwxr-xr-xtest/regress/regress1/sygus/car_3.lus.sy2
-rw-r--r--test/regress/regress1/sygus/clock-inc-tuple.sy2
-rw-r--r--test/regress/regress1/sygus/commutative-stream.sy2
-rw-r--r--test/regress/regress1/sygus/logiccell_help.sy2
-rw-r--r--test/regress/regress1/sygus/sygus-dt.sy2
11 files changed, 53 insertions, 51 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index e8d8fbe3d..eb32beef5 100644
--- 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 11c03de6c..334879993 100644
--- 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 0db05d93c..7d3947bf4 100644
--- 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 889f4d9c9..8050e97f8 100644
--- 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 917c1473a..e169e1a5c 100644
--- 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 e1f37d2cd..8be52a577 100644
--- 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 b572622f7..088613f21 100755
--- 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 43fd7c1ac..65b17605d 100644
--- 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 ae8d0b8c0..7b96a2bf3 100644
--- 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 34f21ba55..1ba05e648 100644
--- 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 d496e3fdc..2f3f4dbb9 100644
--- 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback