From: Andrew Reynolds Date: Fri, 5 Oct 2018 16:13:39 +0000 (-0500) Subject: Update default options for sygus (#2586) X-Git-Tag: cvc5-1.0.0~4454 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1bd02cac69871158d71c74b23aa94c99cd69bead;p=cvc5.git Update default options for sygus (#2586) --- 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::iterator itx = d_examples_invalid.find(e); + std::map::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)