From bf8ec7d9f13a9b37d9b5b279167b77cf28d74c45 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Mar 2022 15:00:14 -0500 Subject: [PATCH] Update checkSynth and checkSynthNext to return SynthResult (#8382) Also extends to non-trivial unit test of SynthResult. Note this also changes the expected output when using --sygus-out=status from unsat/sat/unknown to feasible/infeasible/fail (the option is used mostly just for our regressions). The output mode status-or-def is now equivalent to standard and is hence deleted. --- examples/api/cpp/sygus-fun.cpp | 2 +- examples/api/cpp/sygus-grammar.cpp | 2 +- examples/api/cpp/sygus-inv.cpp | 2 +- examples/api/java/SygusFun.java | 2 +- examples/api/java/SygusGrammar.java | 2 +- examples/api/java/SygusInv.java | 2 +- examples/api/python/sygus-fun.py | 2 +- examples/api/python/sygus-grammar.py | 2 +- examples/api/python/sygus-inv.py | 2 +- src/api/cpp/cvc5.cpp | 4 +-- src/api/cpp/cvc5.h | 16 +++++---- src/api/java/io/github/cvc5/api/Solver.java | 22 ++++++------ src/api/java/jni/solver.cpp | 4 +-- src/api/python/cvc5.pxd | 4 +-- src/api/python/cvc5.pxi | 15 +++++--- src/options/smt_options.toml | 3 -- src/smt/command.cpp | 16 +++++---- src/smt/command.h | 4 +-- src/smt/solver_engine.cpp | 4 +-- src/smt/solver_engine.h | 3 +- src/smt/solver_engine_state.cpp | 7 ++-- src/smt/solver_engine_state.h | 5 +-- src/smt/sygus_solver.cpp | 15 ++++---- src/smt/sygus_solver.h | 4 +-- .../quantifiers/sygus/sygus_interpol.cpp | 8 ++--- .../cli/regress0/sygus/General_plus10.sy | 2 +- test/regress/cli/regress0/sygus/aig-si.sy | 2 +- .../regress0/sygus/array-grammar-select.sy | 2 +- .../cli/regress0/sygus/assume-simple.sy | 2 +- test/regress/cli/regress0/sygus/c100.sy | 2 +- test/regress/cli/regress0/sygus/ccp16.lus.sy | 2 +- .../sygus/cegqi-si-string-triv-2fun.sy | 2 +- .../regress0/sygus/cegqi-si-string-triv.sy | 2 +- .../cli/regress0/sygus/check-generic-red.sy | 2 +- .../cli/regress0/sygus/const-var-test.sy | 2 +- .../cli/regress0/sygus/dt-no-syntax.sy | 2 +- .../cli/regress0/sygus/dt-sel-parse1.sy | 2 +- .../regress0/sygus/hd-05-d1-prog-nogrammar.sy | 2 +- .../cli/regress0/sygus/ho-occ-synth-fun.sy | 2 +- .../regress0/sygus/incremental-modify-ex.sy | 4 +-- .../regress0/sygus/inv-different-var-order.sy | 2 +- test/regress/cli/regress0/sygus/issue3624.sy | 2 +- .../regress0/sygus/issue4383-cache-fv-id.sy | 2 +- .../cli/regress0/sygus/issue4790-dtd.sy | 2 +- .../cli/regress0/sygus/issue6298-par.sy | 2 +- test/regress/cli/regress0/sygus/let-ringer.sy | 2 +- test/regress/cli/regress0/sygus/let-simp.sy | 2 +- test/regress/cli/regress0/sygus/no-logic.sy | 2 +- .../cli/regress0/sygus/no-syntax-test-bool.sy | 2 +- .../cli/regress0/sygus/no-syntax-test.sy | 2 +- .../cli/regress0/sygus/parity-AIG-d0.sy | 2 +- .../cli/regress0/sygus/parse-bv-let.sy | 2 +- .../cli/regress0/sygus/pbe-pred-contra.sy | 2 +- .../regress/cli/regress0/sygus/real-si-all.sy | 2 +- .../regress0/sygus/strings-unconstrained.sy | 2 +- .../regress/cli/regress0/sygus/sygus-no-wf.sy | 2 +- test/regress/cli/regress0/sygus/sygus-uf.sy | 2 +- test/regress/cli/regress0/sygus/uminus_one.sy | 2 +- .../sygus/univ_3-long-repeat-conflict.sy | 2 +- test/regress/cli/regress1/sygus/Base16_1.sy | 2 +- test/regress/cli/regress1/sygus/VC22_a.sy | 2 +- test/regress/cli/regress1/sygus/abv.sy | 2 +- .../cli/regress1/sygus/array-grammar-store.sy | 2 +- test/regress/cli/regress1/sygus/array-uc.sy | 2 +- .../cli/regress1/sygus/array_search_2.sy | 2 +- .../regress1/sygus/array_search_5-Q-easy.sy | 2 +- .../cli/regress1/sygus/array_sum_2_5.sy | 2 +- .../regress/cli/regress1/sygus/bvudiv-by-2.sy | 2 +- test/regress/cli/regress1/sygus/car_3.lus.sy | 2 +- test/regress/cli/regress1/sygus/cegar1.sy | 2 +- .../regress1/sygus/cegis-unif-inv-eq-fair.sy | 2 +- test/regress/cli/regress1/sygus/cggmp.sy | 2 +- .../cli/regress1/sygus/clock-inc-tuple.sy | 2 +- .../cli/regress1/sygus/coeff-solve-inv.sy | 2 +- .../regress/cli/regress1/sygus/commutative.sy | 2 +- .../cli/regress1/sygus/complex-no-rewrite.sy | 2 +- .../regress1/sygus/complex-rewrite-in-db.sy | 2 +- .../regress1/sygus/concat_extract_example.sy | 2 +- .../regress1/sygus/constant-bool-si-all.sy | 2 +- .../regress1/sygus/constant-dec-tree-bug.sy | 2 +- .../cli/regress1/sygus/constant-ite-bv.sy | 2 +- test/regress/cli/regress1/sygus/constant.sy | 2 +- .../cli/regress1/sygus/crci-ssb-unk.sy | 2 +- .../cli/regress1/sygus/crcy-si-rcons.sy | 2 +- test/regress/cli/regress1/sygus/crcy-si.sy | 2 +- test/regress/cli/regress1/sygus/cube-nia.sy | 2 +- .../regress/cli/regress1/sygus/discPresent.sy | 2 +- test/regress/cli/regress1/sygus/double.sy | 2 +- test/regress/cli/regress1/sygus/dt-test-ns.sy | 2 +- test/regress/cli/regress1/sygus/dup-op.sy | 2 +- test/regress/cli/regress1/sygus/eq-sub-obs.sy | 2 +- test/regress/cli/regress1/sygus/error1-dt.sy | 2 +- test/regress/cli/regress1/sygus/eval-uc.sy | 2 +- test/regress/cli/regress1/sygus/extract.sy | 2 +- .../cli/regress1/sygus/fast-enum-backtrack.sy | 2 +- .../cli/regress1/sygus/fg_polynomial3.sy | 2 +- ...ind_inv_eq_bvmul_4bit_withoutgrammar-v2.sy | 2 +- .../cli/regress1/sygus/find_sc_bvult_bvnot.sy | 2 +- .../sygus/ground-ite-free-constant-si.sy | 2 +- .../cli/regress1/sygus/hd-01-d1-prog.sy | 2 +- .../regress1/sygus/hd-19-d1-prog-dup-op.sy | 2 +- test/regress/cli/regress1/sygus/hd-sdiv.sy | 2 +- test/regress/cli/regress1/sygus/ho-sygus.sy | 2 +- .../regress1/sygus/icfp_14.12-flip-args.sy | 2 +- test/regress/cli/regress1/sygus/icfp_14.12.sy | 2 +- .../regress1/sygus/icfp_14_12_diff_types.sy | 2 +- test/regress/cli/regress1/sygus/icfp_28_10.sy | 2 +- .../cli/regress1/sygus/icfp_easy-ite.sy | 2 +- .../regress1/sygus/incremental-stream-ex.sy | 8 ++--- .../cli/regress1/sygus/int-any-const.sy | 2 +- .../regress/cli/regress1/sygus/inv-example.sy | 2 +- .../cli/regress1/sygus/inv-missed-sol-true.sy | 2 +- test/regress/cli/regress1/sygus/inv-unused.sy | 2 +- .../cli/regress1/sygus/inv_gen_fig8.sy | 2 +- test/regress/cli/regress1/sygus/issue2914.sy | 2 +- test/regress/cli/regress1/sygus/issue2935.sy | 2 +- .../cli/regress1/sygus/issue3109-share-sel.sy | 2 +- .../cli/regress1/sygus/issue3320-quant.sy | 2 +- test/regress/cli/regress1/sygus/issue3461.sy | 2 +- test/regress/cli/regress1/sygus/issue3580.sy | 2 +- test/regress/cli/regress1/sygus/issue3649.sy | 2 +- .../sygus/issue3802-default-consts.sy | 2 +- .../cli/regress1/sygus/large-const-simp.sy | 2 +- .../cli/regress1/sygus/let-bug-simp.sy | 2 +- .../regress/cli/regress1/sygus/list-head-x.sy | 2 +- .../cli/regress1/sygus/list_recursor.sy | 2 +- .../cli/regress1/sygus/logiccell_help.sy | 2 +- test/regress/cli/regress1/sygus/max-all.sy | 2 +- test/regress/cli/regress1/sygus/max-limit.sy | 2 +- test/regress/cli/regress1/sygus/max-try1.sy | 2 +- test/regress/cli/regress1/sygus/max-try2.sy | 2 +- test/regress/cli/regress1/sygus/max.sy | 2 +- test/regress/cli/regress1/sygus/max2-bv.sy | 2 +- .../regress1/sygus/multi-fun-polynomial2.sy | 2 +- .../regress/cli/regress1/sygus/nflat-fwd-3.sy | 2 +- test/regress/cli/regress1/sygus/nflat-fwd.sy | 2 +- .../cli/regress1/sygus/nia-max-square-ns.sy | 2 +- .../cli/regress1/sygus/no-flat-simp.sy | 2 +- test/regress/cli/regress1/sygus/no-mention.sy | 2 +- .../cli/regress1/sygus/node-discrete.sy | 8 ++--- test/regress/cli/regress1/sygus/once_2.sy | 2 +- .../cli/regress1/sygus/only-const-grammar.sy | 2 +- .../cli/regress1/sygus/pLTL_5_trace.sy | 2 +- .../cli/regress1/sygus/parity-si-rcons.sy | 2 +- test/regress/cli/regress1/sygus/pbe_multi.sy | 2 +- .../cli/regress1/sygus/phone-1-long.sy | 2 +- .../cli/regress1/sygus/planning-unif.sy | 2 +- .../cli/regress1/sygus/process-10-vars.sy | 2 +- test/regress/cli/regress1/sygus/qe.sy | 2 +- test/regress/cli/regress1/sygus/rand_const.sy | 2 +- test/regress/cli/regress1/sygus/rand_p_0.sy | 2 +- test/regress/cli/regress1/sygus/rand_p_1.sy | 2 +- test/regress/cli/regress1/sygus/re-concat.sy | 2 +- .../cli/regress1/sygus/real-any-const.sy | 2 +- .../cli/regress1/sygus/real-grammar.sy | 2 +- .../cli/regress1/sygus/rec-fun-swap.sy | 2 +- .../cli/regress1/sygus/rec-fun-sygus.sy | 2 +- .../cli/regress1/sygus/rec-fun-while-1.sy | 2 +- .../cli/regress1/sygus/rec-fun-while-2.sy | 2 +- .../regress1/sygus/rec-fun-while-infinite.sy | 2 +- .../cli/regress1/sygus/repair-const-rl.sy | 2 +- .../regress1/sygus/replicate-mod-assume.sy | 2 +- .../cli/regress1/sygus/replicate-mod.sy | 2 +- .../cli/regress1/sygus/rex-strings-alarm.sy | 2 +- .../cli/regress1/sygus/sets-pred-test.sy | 2 +- .../cli/regress1/sygus/simple-no-rewrite.sy | 2 +- .../regress1/sygus/simple-not-in-grammar.sy | 2 +- .../cli/regress1/sygus/simple-regexp.sy | 2 +- .../regress1/sygus/simple-rewrite-in-db.sy | 2 +- .../sygus/simple-rewrite-not-in-db.sy | 2 +- .../cli/regress1/sygus/stopwatch-bt.sy | 2 +- .../cli/regress1/sygus/strings-any-term1.sy | 2 +- .../regress1/sygus/strings-concat-3-args.sy | 2 +- .../cli/regress1/sygus/strings-double-rec.sy | 2 +- .../cli/regress1/sygus/strings-no-syntax.sy | 2 +- .../cli/regress1/sygus/strings-small.sy | 2 +- .../sygus/strings-template-infer-unused.sy | 2 +- .../regress1/sygus/strings-template-infer.sy | 2 +- .../regress1/sygus/strings-trivial-simp.sy | 2 +- .../sygus/strings-trivial-two-type.sy | 2 +- .../cli/regress1/sygus/strings-trivial.sy | 2 +- test/regress/cli/regress1/sygus/sygus-dt.sy | 2 +- .../cli/regress1/sygus/sygus-lambda-fv.sy | 2 +- .../regress/cli/regress1/sygus/sygus-uf-ex.sy | 2 +- test/regress/cli/regress1/sygus/t8.sy | 2 +- .../temp_input_to_synth_ic-error-121418.sy | 2 +- test/regress/cli/regress1/sygus/tester.sy | 2 +- test/regress/cli/regress1/sygus/tl-type-0.sy | 2 +- test/regress/cli/regress1/sygus/tl-type-4x.sy | 2 +- test/regress/cli/regress1/sygus/tl-type.sy | 2 +- .../regress1/sygus/triv-type-mismatch-si.sy | 2 +- test/regress/cli/regress1/sygus/twolets1.sy | 2 +- .../cli/regress1/sygus/twolets2-orig.sy | 2 +- .../cli/regress1/sygus/unbdd_inv_gen_winf1.sy | 2 +- .../cli/regress1/sygus/univ_2-long-repeat.sy | 2 +- test/regress/cli/regress2/sygus/MPwL_d1s3.sy | 2 +- .../cli/regress2/sygus/array_sum_dd.sy | 2 +- .../cli/regress2/sygus/cegisunif-depth1-bv.sy | 2 +- test/regress/cli/regress2/sygus/ex23.sy | 2 +- .../cli/regress2/sygus/examples-deq.sy | 2 +- .../cli/regress2/sygus/icfp_easy_mt_ite.sy | 2 +- .../regress/cli/regress2/sygus/lustre-real.sy | 2 +- test/regress/cli/regress2/sygus/max2-univ.sy | 2 +- test/regress/cli/regress2/sygus/min_IC_1.sy | 2 +- .../cli/regress2/sygus/mpg_guard1-dd.sy | 2 +- test/regress/cli/regress2/sygus/multi-udiv.sy | 2 +- .../cli/regress2/sygus/no-bad-filter.sy | 2 +- .../regress2/sygus/no-syntax-test-no-si.sy | 2 +- test/regress/cli/regress2/sygus/pbe_bvurem.sy | 2 +- .../regress2/sygus/process-10-vars-2fun.sy | 2 +- .../regress2/sygus/process-arg-invariance.sy | 2 +- .../cli/regress2/sygus/proj-issue119.sy | 2 +- .../cli/regress2/sygus/real-grammar-neg.sy | 2 +- .../cli/regress2/sygus/sets-fun-test.sy | 2 +- .../regress2/sygus/strings-no-syntax-len.sy | 2 +- .../cli/regress2/sygus/sumn_recur_synth.sy | 2 +- test/regress/cli/regress2/sygus/three.sy | 2 +- test/regress/cli/regress3/DRAGON_1.lus.sy | 2 +- test/regress/cli/regress3/cegisunif-depth1.sy | 2 +- test/regress/cli/regress3/inv_gen_n_c11.sy | 2 +- test/regress/cli/regress3/nia-max-square.sy | 2 +- test/regress/cli/regress3/policyM.sy | 2 +- test/regress/cli/regress3/sixfuncs.sy | 2 +- test/regress/cli/regress3/strings-any-term.sy | 2 +- .../regress/cli/regress3/unbdd_inv_gen_ex7.sy | 2 +- .../cli/regress3/unifpi-solve-car_1.lus.sy | 2 +- test/regress/cli/regress3/vcb.sy | 2 +- test/unit/api/cpp/solver_black.cpp | 9 +++-- test/unit/api/cpp/synth_result_black.cpp | 36 +++++++++++++++++++ test/unit/api/java/SolverTest.java | 9 +++-- test/unit/api/java/SynthResultTest.java | 32 +++++++++++++++++ test/unit/api/python/test_solver.py | 9 +++-- test/unit/api/python/test_synth_result.py | 26 ++++++++++++++ 233 files changed, 405 insertions(+), 286 deletions(-) diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index 978e55fe6..630598cac 100644 --- a/examples/api/cpp/sygus-fun.cpp +++ b/examples/api/cpp/sygus-fun.cpp @@ -129,7 +129,7 @@ int main() {slv.mkTerm(ADD, {max_x_y, min_x_y}), slv.mkTerm(ADD, {varX, varY})})); // print solutions if available - if (slv.checkSynth().isUnsat()) + if (slv.checkSynth().hasSolution()) { // Output should be equivalent to: // ( diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp index 7be3cb062..4d543039c 100644 --- a/examples/api/cpp/sygus-grammar.cpp +++ b/examples/api/cpp/sygus-grammar.cpp @@ -116,7 +116,7 @@ int main() slv.mkTerm(EQUAL, {{id1_x, id2_x, id3_x, id4_x, varX}})); // print solutions if available - if (slv.checkSynth().isUnsat()) + if (slv.checkSynth().hasSolution()) { // Output should be equivalent to: // ( diff --git a/examples/api/cpp/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp index 3b8edd53a..ba7b5ff93 100644 --- a/examples/api/cpp/sygus-inv.cpp +++ b/examples/api/cpp/sygus-inv.cpp @@ -85,7 +85,7 @@ int main() slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f); // print solutions if available - if (slv.checkSynth().isUnsat()) + if (slv.checkSynth().hasSolution()) { // Output should be equivalent to: // ( diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java index 07a0eebbc..42a93e4f7 100644 --- a/examples/api/java/SygusFun.java +++ b/examples/api/java/SygusFun.java @@ -125,7 +125,7 @@ public class SygusFun slv.mkTerm(EQUAL, slv.mkTerm(ADD, max_x_y, min_x_y), slv.mkTerm(ADD, varX, varY))); // print solutions if available - if (slv.checkSynth().isUnsat()) + if (slv.checkSynth().hasSolution()) { // Output should be equivalent to: // ( diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java index 25233617b..ce59ab9c5 100644 --- a/examples/api/java/SygusGrammar.java +++ b/examples/api/java/SygusGrammar.java @@ -113,7 +113,7 @@ public class SygusGrammar slv.addSygusConstraint(slv.mkTerm(EQUAL, new Term[] {id1_x, id2_x, id3_x, id4_x, varX})); // print solutions if available - if (slv.checkSynth().isUnsat()) + if (slv.checkSynth().hasSolution()) { // Output should be equivalent to: // ( diff --git a/examples/api/java/SygusInv.java b/examples/api/java/SygusInv.java index f07a4816e..f1d611b2e 100644 --- a/examples/api/java/SygusInv.java +++ b/examples/api/java/SygusInv.java @@ -81,7 +81,7 @@ public class SygusInv slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f); // print solutions if available - if (slv.checkSynth().isUnsat()) + if (slv.checkSynth().hasSolution()) { // Output should be equivalent to: // ( diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 82f3d08a7..94cd26d6b 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -90,7 +90,7 @@ if __name__ == "__main__": Kind.Equal, slv.mkTerm(Kind.Add, max_x_y, min_x_y), slv.mkTerm(Kind.Add, varX, varY))) # print solutions if available - if (slv.checkSynth().isUnsat()): + if (slv.checkSynth().hasSolution()): # Output should be equivalent to: # (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) # (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index c6c158f79..7c020e39d 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -82,7 +82,7 @@ if __name__ == "__main__": slv.addSygusConstraint(slv.mkTerm(Kind.And, [slv.mkTerm(Kind.Equal, id1_x, id2_x), slv.mkTerm(Kind.Equal, id1_x, id3_x), slv.mkTerm(Kind.Equal, id1_x, id4_x), slv.mkTerm(Kind.Equal, id1_x, varX)])) # print solutions if available - if (slv.checkSynth().isUnsat()): + if (slv.checkSynth().hasSolution()): # Output should be equivalent to: # (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) # (define-fun id2 ((x Int)) Int x) diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index 90a3deca7..0b96e9ccd 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -58,7 +58,7 @@ if __name__ == "__main__": slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f) # print solutions if available - if slv.checkSynth().isUnsat(): + if slv.checkSynth().hasSolution(): # Output should be equivalent to: # (define-fun inv-f ((x Int)) Bool (not (>= x 11))) terms = [inv_f] diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b229ef65f..8a269a241 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7626,7 +7626,7 @@ void Solver::addSygusInvConstraint(Term inv, CVC5_API_TRY_CATCH_END; } -Result Solver::checkSynth() const +SynthResult Solver::checkSynth() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus) @@ -7637,7 +7637,7 @@ Result Solver::checkSynth() const CVC5_API_TRY_CATCH_END; } -Result Solver::checkSynthNext() const +SynthResult Solver::checkSynthNext() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index a7ed927df..026a7365b 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4752,10 +4752,12 @@ class CVC5_EXPORT Solver * (check-synth) * \endverbatim * - * @return the result of the check, which is unsat if the check succeeded, - * in which case solutions are available via getSynthSolutions. + * @return the result of the check, which is "solution" if the check found a + * solution in which case solutions are available via + * getSynthSolutions, "no solution" if it was determined there is no + * solution, or "unknown" otherwise. */ - Result checkSynth() const; + SynthResult checkSynth() const; /** * Try to find a next solution for the synthesis conjecture corresponding to @@ -4771,10 +4773,12 @@ class CVC5_EXPORT Solver * (check-synth-next) * \endverbatim * - * @return the result of the check, which is unsat if the check succeeded, - * in which case solutions are available via getSynthSolutions. + * @return the result of the check, which is "solution" if the check found a + * solution in which case solutions are available via + * getSynthSolutions, "no solution" if it was determined there is no + * solution, or "unknown" otherwise. */ - Result checkSynthNext() const; + SynthResult checkSynthNext() const; /** * Get the synthesis solution of the given term. This method should be called diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 32b5c4adc..01fe033b4 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -2636,13 +2636,14 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( check-synth ) * } - * @return the result of the check, which is unsat if the check succeeded, - * in which case solutions are available via getSynthSolutions. + * @return the result of the check, which is "solution" if the check found a + * solution in which case solutions are available via + * getSynthSolutions, "no solution" if it was determined there is no + * solution, or "unknown" otherwise. */ - public Result checkSynth() - { + public SynthResult checkSynth() { long resultPointer = checkSynth(pointer); - return new Result(this, resultPointer); + return new SynthResult(this, resultPointer); } private native long checkSynth(long pointer); @@ -2656,13 +2657,14 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( check-synth-next ) * } - * @return the result of the check, which is UNSAT if the check succeeded, - * in which case solutions are available via getSynthSolutions. + * @return the result of the check, which is "solution" if the check found a + * solution in which case solutions are available via + * getSynthSolutions, "no solution" if it was determined there is no + * solution, or "unknown" otherwise. */ - public Result checkSynthNext() - { + public SynthResult checkSynthNext() { long resultPointer = checkSynthNext(pointer); - return new Result(this, resultPointer); + return new SynthResult(this, resultPointer); } private native long checkSynthNext(long pointer); diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 87caff1b0..b8a2e2739 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2608,7 +2608,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynth(JNIEnv* env, { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); - Result* retPointer = new Result(solver->checkSynth()); + SynthResult* retPointer = new SynthResult(solver->checkSynth()); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } @@ -2623,7 +2623,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynthNext( { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); - Result* retPointer = new Result(solver->checkSynthNext()); + SynthResult* retPointer = new SynthResult(solver->checkSynthNext()); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index f133f324d..a5ca0470e 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -252,8 +252,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": void addSygusInvConstraint(Term inv_f, Term pre_f, Term trans_f, Term post_f) except + Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort) except + Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort, Grammar grammar) except + - Result checkSynth() except + - Result checkSynthNext() except + + SynthResult checkSynth() except + + SynthResult checkSynthNext() except + Term getSynthSolution(Term t) except + vector[Term] getSynthSolutions(const vector[Term]& terms) except + Term synthInv(const string& symbol, const vector[Term]& bound_vars) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 354adaed1..cece9c3fb 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1678,9 +1678,12 @@ cdef class Solver: ( check-synth ) - :return: the result of the synthesis conjecture. + :return: the result of the check, which is "solution" if the check + found a solution in which case solutions are available via + getSynthSolutions, "no solution" if it was determined there is + no solution, or "unknown" otherwise. """ - cdef Result r = Result() + cdef SynthResult r = SynthResult() r.cr = self.csolver.checkSynth() return r @@ -1697,10 +1700,12 @@ cdef class Solver: ( check-synth ) - :return: the result of the check, which is unsat if the check succeeded, - in which case solutions are available via getSynthSolutions. + :return: the result of the check, which is "solution" if the check + found a solution in which case solutions are available via + getSynthSolutions, "no solution" if it was determined there is + no solution, or "unknown" otherwise. """ - cdef Result r = Result() + cdef SynthResult r = SynthResult() r.cr = self.csolver.checkSynthNext() return r diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 3b3f9e240..30da2e1de 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -165,9 +165,6 @@ name = "SMT Layer" [[option.mode.STATUS_AND_DEF]] name = "status-and-def" help = "Print status followed by definition corresponding to solution." -[[option.mode.STATUS_OR_DEF]] - name = "status-or-def" - help = "Print status if infeasible, or definition corresponding to solution if feasible." [[option.mode.STANDARD]] name = "sygus-standard" help = "Print based on SyGuS standard." diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 04dbc77bb..f7772dab6 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -774,21 +774,25 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm) d_commandStatus = CommandSuccess::instance(); d_solution.clear(); // check whether we should print the status - if (!d_result.isUnsat() + if (!d_result.hasSolution() || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF || options::sygusOut() == options::SygusSolutionOutMode::STATUS) { - if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD) + if (d_result.hasSolution()) { - d_solution << "fail" << endl; + d_solution << "feasible" << std::endl; + } + else if (d_result.hasNoSolution()) + { + d_solution << "infeasible" << std::endl; } else { - d_solution << d_result << endl; + d_solution << "fail" << std::endl; } } // check whether we should print the solution - if (d_result.isUnsat() + if (d_result.hasSolution() && options::sygusOut() != options::SygusSolutionOutMode::STATUS) { std::vector synthFuns = sm->getFunctionsToSynthesize(); @@ -823,7 +827,7 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -api::Result CheckSynthCommand::getResult() const { return d_result; } +api::SynthResult CheckSynthCommand::getResult() const { return d_result; } void CheckSynthCommand::printResult(std::ostream& out) const { if (!ok()) diff --git a/src/smt/command.h b/src/smt/command.h index 66c678ba8..3e4997878 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -823,7 +823,7 @@ class CVC5_EXPORT CheckSynthCommand : public Command public: CheckSynthCommand(bool isNext = false) : d_isNext(isNext){}; /** returns the result of the check-synth call */ - api::Result getResult() const; + api::SynthResult getResult() const; /** prints the result of the check-synth-call */ void printResult(std::ostream& out) const override; /** invokes this command @@ -849,7 +849,7 @@ class CVC5_EXPORT CheckSynthCommand : public Command /** Whether this is a check-synth-next call */ bool d_isNext; /** result of the check-synth call */ - api::Result d_result; + api::SynthResult d_result; /** string stream that stores the output of the solution */ std::stringstream d_solution; }; diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 78e0a40b3..65acec2ee 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -892,7 +892,7 @@ void SolverEngine::assertSygusInvConstraint(Node inv, d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); } -Result SolverEngine::checkSynth(bool isNext) +SynthResult SolverEngine::checkSynth(bool isNext) { SolverEngineScope smts(this); finishInit(); @@ -902,7 +902,7 @@ Result SolverEngine::checkSynth(bool isNext) "Cannot check-synth-next unless immediately preceded by a successful " "call to check-synth(-next)."); } - Result r = d_sygusSolver->checkSynth(*d_asserts, isNext); + SynthResult r = d_sygusSolver->checkSynth(*d_asserts, isNext); d_state->notifyCheckSynthResult(r); return r; } diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 1b186c247..6837c97a7 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -29,6 +29,7 @@ #include "smt/smt_mode.h" #include "theory/logic_info.h" #include "util/result.h" +#include "util/synth_result.h" namespace cvc5 { @@ -448,7 +449,7 @@ class CVC5_EXPORT SolverEngine * * @throw Exception */ - Result checkSynth(bool isNext = false); + SynthResult checkSynth(bool isNext = false); /*------------------------- end of sygus commands ------------------------*/ diff --git a/src/smt/solver_engine_state.cpp b/src/smt/solver_engine_state.cpp index 3cab423ab..68a40b009 100644 --- a/src/smt/solver_engine_state.cpp +++ b/src/smt/solver_engine_state.cpp @@ -84,7 +84,8 @@ void SolverEngineState::notifyCheckSat(bool hasAssumptions) } } -void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) +void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, + const Result& r) { d_needPostsolve = true; @@ -118,9 +119,9 @@ void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) } } -void SolverEngineState::notifyCheckSynthResult(Result r) +void SolverEngineState::notifyCheckSynthResult(const SynthResult& r) { - if (r.getStatus() == Result::UNSAT) + if (r.getStatus() == SynthResult::SOLUTION) { // successfully generated a synthesis solution, update to abduct state d_smtMode = SmtMode::SYNTH; diff --git a/src/smt/solver_engine_state.h b/src/smt/solver_engine_state.h index 5cc72fd08..ac1a25e70 100644 --- a/src/smt/solver_engine_state.h +++ b/src/smt/solver_engine_state.h @@ -24,6 +24,7 @@ #include "smt/env_obj.h" #include "smt/smt_mode.h" #include "util/result.h" +#include "util/synth_result.h" namespace cvc5 { @@ -86,12 +87,12 @@ class SolverEngineState : protected EnvObj * If so, we pop a context. * @param r The result of the check-sat call. */ - void notifyCheckSatResult(bool hasAssumptions, Result r); + void notifyCheckSatResult(bool hasAssumptions, const Result& r); /** * Notify that the result of the last check-synth or check-synth-next was r. * @param r The result of the check-synth or check-synth-next call. */ - void notifyCheckSynthResult(Result r); + void notifyCheckSynthResult(const SynthResult& r); /** * Notify that we finished an abduction query, where success is whether the * command was successful. This is managed independently of the above diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 9ffdfc438..f1762fb58 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -183,7 +183,7 @@ void SygusSolver::assertSygusInvConstraint(Node inv, d_sygusConjectureStale = true; } -Result SygusSolver::checkSynth(Assertions& as, bool isNext) +SynthResult SygusSolver::checkSynth(Assertions& as, bool isNext) { Trace("smt") << "SygusSolver::checkSynth" << std::endl; // if applicable, check if the subsolver is the correct one @@ -264,8 +264,8 @@ Result SygusSolver::checkSynth(Assertions& as, bool isNext) // The result returned by the above call is typically "unknown", which may // or may not correspond to a state in which we solved the conjecture // successfully. Instead we call getSynthSolutions below. If this returns - // true, then we were successful. In this case, we set the result to "unsat", - // since the synthesis conjecture was negated when asserted to the subsolver. + // true, then we were successful. In this case, we set the synthesis result to + // "solution". // // This behavior is done for 2 reasons: // (1) if we do not negate the synthesis conjecture, the subsolver in some @@ -286,11 +286,12 @@ Result SygusSolver::checkSynth(Assertions& as, bool isNext) // // Thus, we use getSynthSolutions as means of knowing the conjecture was // solved. + SynthResult sr; std::map sol_map; if (getSynthSolutions(sol_map)) { - // if we have solutions, we return "unsat" by convention - r = Result(Result::UNSAT); + // if we have solutions, we return "solution" + sr = SynthResult(SynthResult::SOLUTION); // Check that synthesis solutions satisfy the conjecture if (options().smt.checkSynthSol) { @@ -300,9 +301,9 @@ Result SygusSolver::checkSynth(Assertions& as, bool isNext) else { // otherwise, we return "unknown" - r = Result(Result::UNKNOWN, Result::UNKNOWN_REASON); + sr = SynthResult(SynthResult::UNKNOWN, Result::UNKNOWN_REASON); } - return r; + return sr; } bool SygusSolver::getSynthSolutions(std::map& solMap) diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index b37762ce1..6530f532b 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -24,7 +24,7 @@ #include "expr/type_node.h" #include "smt/assertions.h" #include "smt/env_obj.h" -#include "util/result.h" +#include "util/synth_result.h" namespace cvc5 { @@ -131,7 +131,7 @@ class SygusSolver : protected EnvObj * in which f1...fn are the functions-to-synthesize, v1...vm are the declared * universal variables and F is the set of declared constraints. */ - Result checkSynth(Assertions& as, bool isNext); + SynthResult checkSynth(Assertions& as, bool isNext); /** * Get synth solution. * diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 4787b65db..a217b375e 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -346,10 +346,10 @@ bool SygusInterpol::solveInterpolation(const std::string& name, Trace("sygus-interpol") << " SygusInterpol::solveInterpolation check synth..." << std::endl; - Result r = d_subSolver->checkSynth(); + SynthResult r = d_subSolver->checkSynth(); Trace("sygus-interpol") << " SygusInterpol::solveInterpolation result: " << r << std::endl; - if (r.getStatus() == Result::UNSAT) + if (r.getStatus() == SynthResult::SOLUTION) { return findInterpol(d_subSolver.get(), interpol, d_itp); } @@ -361,10 +361,10 @@ bool SygusInterpol::solveInterpolationNext(Node& interpol) Trace("sygus-interpol") << " SygusInterpol::solveInterpolationNext check synth..." << std::endl; // invoke the check-synth with isNext = true. - Result r = d_subSolver->checkSynth(true); + SynthResult r = d_subSolver->checkSynth(true); Trace("sygus-interpol") << " SygusInterpol::solveInterpolationNext result: " << r << std::endl; - if (r.getStatus() == Result::UNSAT) + if (r.getStatus() == SynthResult::SOLUTION) { return findInterpol(d_subSolver.get(), interpol, d_itp); } diff --git a/test/regress/cli/regress0/sygus/General_plus10.sy b/test/regress/cli/regress0/sygus/General_plus10.sy index 9dee4efdf..42fb39858 100755 --- a/test/regress/cli/regress0/sygus/General_plus10.sy +++ b/test/regress/cli/regress0/sygus/General_plus10.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress0/sygus/aig-si.sy b/test/regress/cli/regress0/sygus/aig-si.sy index 3b8be96fd..238c558ee 100644 --- a/test/regress/cli/regress0/sygus/aig-si.sy +++ b/test/regress/cli/regress0/sygus/aig-si.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress0/sygus/array-grammar-select.sy b/test/regress/cli/regress0/sygus/array-grammar-select.sy index 2c0b4cf9a..51c5665a2 100644 --- a/test/regress/cli/regress0/sygus/array-grammar-select.sy +++ b/test/regress/cli/regress0/sygus/array-grammar-select.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALIA) diff --git a/test/regress/cli/regress0/sygus/assume-simple.sy b/test/regress/cli/regress0/sygus/assume-simple.sy index 58f3753d8..ee2aa650e 100644 --- a/test/regress/cli/regress0/sygus/assume-simple.sy +++ b/test/regress/cli/regress0/sygus/assume-simple.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress0/sygus/c100.sy b/test/regress/cli/regress0/sygus/c100.sy index b0837e341..b75ad20d8 100644 --- a/test/regress/cli/regress0/sygus/c100.sy +++ b/test/regress/cli/regress0/sygus/c100.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress0/sygus/ccp16.lus.sy b/test/regress/cli/regress0/sygus/ccp16.lus.sy index 91fe27b0b..8df131a5b 100644 --- a/test/regress/cli/regress0/sygus/ccp16.lus.sy +++ b/test/regress/cli/regress0/sygus/ccp16.lus.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SAT) diff --git a/test/regress/cli/regress0/sygus/cegqi-si-string-triv-2fun.sy b/test/regress/cli/regress0/sygus/cegqi-si-string-triv-2fun.sy index 8fe64697b..e68933356 100644 --- a/test/regress/cli/regress0/sygus/cegqi-si-string-triv-2fun.sy +++ b/test/regress/cli/regress0/sygus/cegqi-si-string-triv-2fun.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress0/sygus/cegqi-si-string-triv.sy b/test/regress/cli/regress0/sygus/cegqi-si-string-triv.sy index f5ce07ec6..edae133cf 100644 --- a/test/regress/cli/regress0/sygus/cegqi-si-string-triv.sy +++ b/test/regress/cli/regress0/sygus/cegqi-si-string-triv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress0/sygus/check-generic-red.sy b/test/regress/cli/regress0/sygus/check-generic-red.sy index c1ebc52b2..7b6a91eb5 100644 --- a/test/regress/cli/regress0/sygus/check-generic-red.sy +++ b/test/regress/cli/regress0/sygus/check-generic-red.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification (set-logic LIA) diff --git a/test/regress/cli/regress0/sygus/const-var-test.sy b/test/regress/cli/regress0/sygus/const-var-test.sy index 78029cbc8..85957e998 100644 --- a/test/regress/cli/regress0/sygus/const-var-test.sy +++ b/test/regress/cli/regress0/sygus/const-var-test.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress0/sygus/dt-no-syntax.sy b/test/regress/cli/regress0/sygus/dt-no-syntax.sy index e33edf36c..870d94e22 100644 --- a/test/regress/cli/regress0/sygus/dt-no-syntax.sy +++ b/test/regress/cli/regress0/sygus/dt-no-syntax.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/cli/regress0/sygus/dt-sel-parse1.sy b/test/regress/cli/regress0/sygus/dt-sel-parse1.sy index 05ba6b85e..15efe28b6 100644 --- a/test/regress/cli/regress0/sygus/dt-sel-parse1.sy +++ b/test/regress/cli/regress0/sygus/dt-sel-parse1.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic ALL) (declare-datatypes ((IntRange 0)) diff --git a/test/regress/cli/regress0/sygus/hd-05-d1-prog-nogrammar.sy b/test/regress/cli/regress0/sygus/hd-05-d1-prog-nogrammar.sy index 8c77eea61..0878f3bd0 100644 --- a/test/regress/cli/regress0/sygus/hd-05-d1-prog-nogrammar.sy +++ b/test/regress/cli/regress0/sygus/hd-05-d1-prog-nogrammar.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none -; EXPECT: unsat +; EXPECT: feasible (set-logic BV) diff --git a/test/regress/cli/regress0/sygus/ho-occ-synth-fun.sy b/test/regress/cli/regress0/sygus/ho-occ-synth-fun.sy index 4bef02b69..0db67a112 100644 --- a/test/regress/cli/regress0/sygus/ho-occ-synth-fun.sy +++ b/test/regress/cli/regress0/sygus/ho-occ-synth-fun.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic HO_ALL) (synth-fun f ((x Int)) Int) (synth-fun g ((x Int)) Int) diff --git a/test/regress/cli/regress0/sygus/incremental-modify-ex.sy b/test/regress/cli/regress0/sygus/incremental-modify-ex.sy index f453964b0..d7e8379df 100644 --- a/test/regress/cli/regress0/sygus/incremental-modify-ex.sy +++ b/test/regress/cli/regress0/sygus/incremental-modify-ex.sy @@ -1,6 +1,6 @@ ; COMMAND-LINE: -i --sygus-out=status -;EXPECT: unsat -;EXPECT: unsat +;EXPECT: feasible +;EXPECT: feasible (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int diff --git a/test/regress/cli/regress0/sygus/inv-different-var-order.sy b/test/regress/cli/regress0/sygus/inv-different-var-order.sy index 7b7d50e22..3462362ca 100644 --- a/test/regress/cli/regress0/sygus/inv-different-var-order.sy +++ b/test/regress/cli/regress0/sygus/inv-different-var-order.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -;EXPECT: unsat +;EXPECT: feasible (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) (define-fun pre-f ((x Int) (y Int) (b Bool)) Bool diff --git a/test/regress/cli/regress0/sygus/issue3624.sy b/test/regress/cli/regress0/sygus/issue3624.sy index 992965432..1f054595e 100644 --- a/test/regress/cli/regress0/sygus/issue3624.sy +++ b/test/regress/cli/regress0/sygus/issue3624.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (declare-var A Bool) diff --git a/test/regress/cli/regress0/sygus/issue4383-cache-fv-id.sy b/test/regress/cli/regress0/sygus/issue4383-cache-fv-id.sy index 27378d9ca..11860a82d 100644 --- a/test/regress/cli/regress0/sygus/issue4383-cache-fv-id.sy +++ b/test/regress/cli/regress0/sygus/issue4383-cache-fv-id.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (synth-fun args_0_refinement_0 diff --git a/test/regress/cli/regress0/sygus/issue4790-dtd.sy b/test/regress/cli/regress0/sygus/issue4790-dtd.sy index 55f4723ec..0348e0ac9 100644 --- a/test/regress/cli/regress0/sygus/issue4790-dtd.sy +++ b/test/regress/cli/regress0/sygus/issue4790-dtd.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status (set-logic NIA) (synth-fun patternGen ((i Int)) Int diff --git a/test/regress/cli/regress0/sygus/issue6298-par.sy b/test/regress/cli/regress0/sygus/issue6298-par.sy index bffa02b29..b083af93c 100644 --- a/test/regress/cli/regress0/sygus/issue6298-par.sy +++ b/test/regress/cli/regress0/sygus/issue6298-par.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (declare-datatypes (( List 1)) ( (par (T) ((nil) (cons (head T) (tail (List T))))))) diff --git a/test/regress/cli/regress0/sygus/let-ringer.sy b/test/regress/cli/regress0/sygus/let-ringer.sy index 9793c927b..918705118 100644 --- a/test/regress/cli/regress0/sygus/let-ringer.sy +++ b/test/regress/cli/regress0/sygus/let-ringer.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-unif-pi=complete --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress0/sygus/let-simp.sy b/test/regress/cli/regress0/sygus/let-simp.sy index 19a4e6bc9..bf28ff0eb 100644 --- a/test/regress/cli/regress0/sygus/let-simp.sy +++ b/test/regress/cli/regress0/sygus/let-simp.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) (define-fun letf ((z Int)) Int (+ z z)) diff --git a/test/regress/cli/regress0/sygus/no-logic.sy b/test/regress/cli/regress0/sygus/no-logic.sy index fd63506d2..f32b7efd9 100644 --- a/test/regress/cli/regress0/sygus/no-logic.sy +++ b/test/regress/cli/regress0/sygus/no-logic.sy @@ -4,7 +4,7 @@ ; EXPECT-ERROR: no-logic.sy:8.10: cvc5 will make all theories available. ; EXPECT-ERROR: no-logic.sy:8.10: Consider setting a stricter logic for (likely) better performance. ; EXPECT-ERROR: no-logic.sy:8.10: To suppress this warning in the future use (set-logic ALL). -; EXPECT: unsat +; EXPECT: feasible (synth-fun f ((x Int)) Int ((Start Int)) ( diff --git a/test/regress/cli/regress0/sygus/no-syntax-test-bool.sy b/test/regress/cli/regress0/sygus/no-syntax-test-bool.sy index 4978b7a57..92d72c6eb 100644 --- a/test/regress/cli/regress0/sygus/no-syntax-test-bool.sy +++ b/test/regress/cli/regress0/sygus/no-syntax-test-bool.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress0/sygus/no-syntax-test.sy b/test/regress/cli/regress0/sygus/no-syntax-test.sy index 696d413ad..675f087d9 100644 --- a/test/regress/cli/regress0/sygus/no-syntax-test.sy +++ b/test/regress/cli/regress0/sygus/no-syntax-test.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress0/sygus/parity-AIG-d0.sy b/test/regress/cli/regress0/sygus/parity-AIG-d0.sy index d3ca69e96..8bfe4a2e6 100644 --- a/test/regress/cli/regress0/sygus/parity-AIG-d0.sy +++ b/test/regress/cli/regress0/sygus/parity-AIG-d0.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress0/sygus/parse-bv-let.sy b/test/regress/cli/regress0/sygus/parse-bv-let.sy index 60bb804b6..c32844e78 100644 --- a/test/regress/cli/regress0/sygus/parse-bv-let.sy +++ b/test/regress/cli/regress0/sygus/parse-bv-let.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress0/sygus/pbe-pred-contra.sy b/test/regress/cli/regress0/sygus/pbe-pred-contra.sy index 927d1bf0e..ff8bedd78 100644 --- a/test/regress/cli/regress0/sygus/pbe-pred-contra.sy +++ b/test/regress/cli/regress0/sygus/pbe-pred-contra.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status -q -; EXPECT: unknown +; EXPECT: fail (set-logic LIA) (synth-fun P ((x Int)) Bool) (constraint (P 54)) diff --git a/test/regress/cli/regress0/sygus/real-si-all.sy b/test/regress/cli/regress0/sygus/real-si-all.sy index 26524cdf6..fa108005c 100644 --- a/test/regress/cli/regress0/sygus/real-si-all.sy +++ b/test/regress/cli/regress0/sygus/real-si-all.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LRA) diff --git a/test/regress/cli/regress0/sygus/strings-unconstrained.sy b/test/regress/cli/regress0/sygus/strings-unconstrained.sy index 49272165d..faad97a3a 100644 --- a/test/regress/cli/regress0/sygus/strings-unconstrained.sy +++ b/test/regress/cli/regress0/sygus/strings-unconstrained.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun f ((firstname String) (lastname String)) String diff --git a/test/regress/cli/regress0/sygus/sygus-no-wf.sy b/test/regress/cli/regress0/sygus/sygus-no-wf.sy index e89d07fd9..e34c30f5a 100644 --- a/test/regress/cli/regress0/sygus/sygus-no-wf.sy +++ b/test/regress/cli/regress0/sygus/sygus-no-wf.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic ALL) (synth-fun f ((x0 Bool)) Bool ((B Bool) (I Int)) diff --git a/test/regress/cli/regress0/sygus/sygus-uf.sy b/test/regress/cli/regress0/sygus/sygus-uf.sy index 2f59598ec..b05fe31e5 100644 --- a/test/regress/cli/regress0/sygus/sygus-uf.sy +++ b/test/regress/cli/regress0/sygus/sygus-uf.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic HO_ALL) (declare-var uf (-> Int Int)) diff --git a/test/regress/cli/regress0/sygus/uminus_one.sy b/test/regress/cli/regress0/sygus/uminus_one.sy index 9024ac3b6..87489735b 100644 --- a/test/regress/cli/regress0/sygus/uminus_one.sy +++ b/test/regress/cli/regress0/sygus/uminus_one.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int)) ((Start Int ((- 1))))) diff --git a/test/regress/cli/regress0/sygus/univ_3-long-repeat-conflict.sy b/test/regress/cli/regress0/sygus/univ_3-long-repeat-conflict.sy index abcccd2ab..aada8f7dc 100644 --- a/test/regress/cli/regress0/sygus/univ_3-long-repeat-conflict.sy +++ b/test/regress/cli/regress0/sygus/univ_3-long-repeat-conflict.sy @@ -1,4 +1,4 @@ -; EXPECT: unknown +; EXPECT: fail ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -q (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/Base16_1.sy b/test/regress/cli/regress1/sygus/Base16_1.sy index b47060bf8..05b457e74 100644 --- a/test/regress/cli/regress1/sygus/Base16_1.sy +++ b/test/regress/cli/regress1/sygus/Base16_1.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cegqi-full --sygus-out=status --sygus-si=all (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/VC22_a.sy b/test/regress/cli/regress1/sygus/VC22_a.sy index f60f661dd..5d27d649a 100644 --- a/test/regress/cli/regress1/sygus/VC22_a.sy +++ b/test/regress/cli/regress1/sygus/VC22_a.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegis-sample=use (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/abv.sy b/test/regress/cli/regress1/sygus/abv.sy index d42553c1b..be8b755f9 100644 --- a/test/regress/cli/regress1/sygus/abv.sy +++ b/test/regress/cli/regress1/sygus/abv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ABV) diff --git a/test/regress/cli/regress1/sygus/array-grammar-store.sy b/test/regress/cli/regress1/sygus/array-grammar-store.sy index 025a17b15..61ba2063e 100644 --- a/test/regress/cli/regress1/sygus/array-grammar-store.sy +++ b/test/regress/cli/regress1/sygus/array-grammar-store.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ABV) diff --git a/test/regress/cli/regress1/sygus/array-uc.sy b/test/regress/cli/regress1/sygus/array-uc.sy index b3d950436..1d43efede 100644 --- a/test/regress/cli/regress1/sygus/array-uc.sy +++ b/test/regress/cli/regress1/sygus/array-uc.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic ALL) (declare-sort U 0) (synth-fun f ((x (Array U Int)) (y U)) Bool) diff --git a/test/regress/cli/regress1/sygus/array_search_2.sy b/test/regress/cli/regress1/sygus/array_search_2.sy index 9009c8260..3c0253c9e 100644 --- a/test/regress/cli/regress1/sygus/array_search_2.sy +++ b/test/regress/cli/regress1/sygus/array_search_2.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) (synth-fun findIdx ((y1 Int) (y2 Int) (k1 Int)) Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) diff --git a/test/regress/cli/regress1/sygus/array_search_5-Q-easy.sy b/test/regress/cli/regress1/sygus/array_search_5-Q-easy.sy index fb1c10337..759122e2c 100644 --- a/test/regress/cli/regress1/sygus/array_search_5-Q-easy.sy +++ b/test/regress/cli/regress1/sygus/array_search_5-Q-easy.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/array_sum_2_5.sy b/test/regress/cli/regress1/sygus/array_sum_2_5.sy index 9490f73b6..e0be37280 100644 --- a/test/regress/cli/regress1/sygus/array_sum_2_5.sy +++ b/test/regress/cli/regress1/sygus/array_sum_2_5.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) diff --git a/test/regress/cli/regress1/sygus/bvudiv-by-2.sy b/test/regress/cli/regress1/sygus/bvudiv-by-2.sy index 2bd8fc0dc..8a29db5ee 100644 --- a/test/regress/cli/regress1/sygus/bvudiv-by-2.sy +++ b/test/regress/cli/regress1/sygus/bvudiv-by-2.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/car_3.lus.sy b/test/regress/cli/regress1/sygus/car_3.lus.sy index 3b58a997c..697443d36 100755 --- a/test/regress/cli/regress1/sygus/car_3.lus.sy +++ b/test/regress/cli/regress1/sygus/car_3.lus.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/cegar1.sy b/test/regress/cli/regress1/sygus/cegar1.sy index d3b2030de..2fe42609c 100644 --- a/test/regress/cli/regress1/sygus/cegar1.sy +++ b/test/regress/cli/regress1/sygus/cegar1.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=post --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/cegis-unif-inv-eq-fair.sy b/test/regress/cli/regress1/sygus/cegis-unif-inv-eq-fair.sy index c3b09011c..d1253b1b4 100644 --- a/test/regress/cli/regress1/sygus/cegis-unif-inv-eq-fair.sy +++ b/test/regress/cli/regress1/sygus/cegis-unif-inv-eq-fair.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/cggmp.sy b/test/regress/cli/regress1/sygus/cggmp.sy index 551528633..a24ba2781 100644 --- a/test/regress/cli/regress1/sygus/cggmp.sy +++ b/test/regress/cli/regress1/sygus/cggmp.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=pre --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/clock-inc-tuple.sy b/test/regress/cli/regress1/sygus/clock-inc-tuple.sy index 5af4407f7..f16e3a5b8 100644 --- a/test/regress/cli/regress1/sygus/clock-inc-tuple.sy +++ b/test/regress/cli/regress1/sygus/clock-inc-tuple.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/coeff-solve-inv.sy b/test/regress/cli/regress1/sygus/coeff-solve-inv.sy index ed4689fe9..0005b6864 100644 --- a/test/regress/cli/regress1/sygus/coeff-solve-inv.sy +++ b/test/regress/cli/regress1/sygus/coeff-solve-inv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2 --sygus-grammar-cons=any-const (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/commutative.sy b/test/regress/cli/regress1/sygus/commutative.sy index 7fe07c3fa..48ef2ce0b 100644 --- a/test/regress/cli/regress1/sygus/commutative.sy +++ b/test/regress/cli/regress1/sygus/commutative.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/complex-no-rewrite.sy b/test/regress/cli/regress1/sygus/complex-no-rewrite.sy index 5a2d38cb8..bfc05f623 100644 --- a/test/regress/cli/regress1/sygus/complex-no-rewrite.sy +++ b/test/regress/cli/regress1/sygus/complex-no-rewrite.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/complex-rewrite-in-db.sy b/test/regress/cli/regress1/sygus/complex-rewrite-in-db.sy index e3e017cec..e3a4990cd 100644 --- a/test/regress/cli/regress1/sygus/complex-rewrite-in-db.sy +++ b/test/regress/cli/regress1/sygus/complex-rewrite-in-db.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/concat_extract_example.sy b/test/regress/cli/regress1/sygus/concat_extract_example.sy index 7d6690816..bc95582fe 100644 --- a/test/regress/cli/regress1/sygus/concat_extract_example.sy +++ b/test/regress/cli/regress1/sygus/concat_extract_example.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic BV) (synth-fun f (( x (_ BitVec 32))) (_ BitVec 32) diff --git a/test/regress/cli/regress1/sygus/constant-bool-si-all.sy b/test/regress/cli/regress1/sygus/constant-bool-si-all.sy index 18a60f176..d3239e724 100644 --- a/test/regress/cli/regress1/sygus/constant-bool-si-all.sy +++ b/test/regress/cli/regress1/sygus/constant-bool-si-all.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun f () Bool) diff --git a/test/regress/cli/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/cli/regress1/sygus/constant-dec-tree-bug.sy index ddbf07d61..32bf9dfd4 100644 --- a/test/regress/cli/regress1/sygus/constant-dec-tree-bug.sy +++ b/test/regress/cli/regress1/sygus/constant-dec-tree-bug.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=complete (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/constant-ite-bv.sy b/test/regress/cli/regress1/sygus/constant-ite-bv.sy index 356c71d1d..5a79f074f 100644 --- a/test/regress/cli/regress1/sygus/constant-ite-bv.sy +++ b/test/regress/cli/regress1/sygus/constant-ite-bv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-repair-const (set-logic BV) (synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64) diff --git a/test/regress/cli/regress1/sygus/constant.sy b/test/regress/cli/regress1/sygus/constant.sy index 1416d566d..469f448ae 100644 --- a/test/regress/cli/regress1/sygus/constant.sy +++ b/test/regress/cli/regress1/sygus/constant.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/crci-ssb-unk.sy b/test/regress/cli/regress1/sygus/crci-ssb-unk.sy index d59fd297d..791bb0242 100644 --- a/test/regress/cli/regress1/sygus/crci-ssb-unk.sy +++ b/test/regress/cli/regress1/sygus/crci-ssb-unk.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/crcy-si-rcons.sy b/test/regress/cli/regress1/sygus/crcy-si-rcons.sy index 177a33274..6e503ab86 100644 --- a/test/regress/cli/regress1/sygus/crcy-si-rcons.sy +++ b/test/regress/cli/regress1/sygus/crcy-si-rcons.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --sygus-si-rcons=try --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/crcy-si.sy b/test/regress/cli/regress1/sygus/crcy-si.sy index 1c0abc4fe..38a7bc3ca 100644 --- a/test/regress/cli/regress1/sygus/crcy-si.sy +++ b/test/regress/cli/regress1/sygus/crcy-si.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/cube-nia.sy b/test/regress/cli/regress1/sygus/cube-nia.sy index ef57840fe..ce06e54e4 100644 --- a/test/regress/cli/regress1/sygus/cube-nia.sy +++ b/test/regress/cli/regress1/sygus/cube-nia.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic NIA) diff --git a/test/regress/cli/regress1/sygus/discPresent.sy b/test/regress/cli/regress1/sygus/discPresent.sy index e089dafa5..3d6c01a07 100644 --- a/test/regress/cli/regress1/sygus/discPresent.sy +++ b/test/regress/cli/regress1/sygus/discPresent.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) ;declare enums diff --git a/test/regress/cli/regress1/sygus/double.sy b/test/regress/cli/regress1/sygus/double.sy index 0ba822278..5e3c25bd7 100644 --- a/test/regress/cli/regress1/sygus/double.sy +++ b/test/regress/cli/regress1/sygus/double.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/dt-test-ns.sy b/test/regress/cli/regress1/sygus/dt-test-ns.sy index f67784002..0df9056d4 100644 --- a/test/regress/cli/regress1/sygus/dt-test-ns.sy +++ b/test/regress/cli/regress1/sygus/dt-test-ns.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic DTLIA) diff --git a/test/regress/cli/regress1/sygus/dup-op.sy b/test/regress/cli/regress1/sygus/dup-op.sy index dfd99f55d..62b81c967 100644 --- a/test/regress/cli/regress1/sygus/dup-op.sy +++ b/test/regress/cli/regress1/sygus/dup-op.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int diff --git a/test/regress/cli/regress1/sygus/eq-sub-obs.sy b/test/regress/cli/regress1/sygus/eq-sub-obs.sy index 69399e293..0dac347e8 100644 --- a/test/regress/cli/regress1/sygus/eq-sub-obs.sy +++ b/test/regress/cli/regress1/sygus/eq-sub-obs.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible ; This regression tests the behavior of the reconstruction algorithm when the ; term to reconstruct contains two equivalent sub-terms, but one is easier to diff --git a/test/regress/cli/regress1/sygus/error1-dt.sy b/test/regress/cli/regress1/sygus/error1-dt.sy index 31308d62a..9b88dadd4 100644 --- a/test/regress/cli/regress1/sygus/error1-dt.sy +++ b/test/regress/cli/regress1/sygus/error1-dt.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-enum=fast (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/eval-uc.sy b/test/regress/cli/regress1/sygus/eval-uc.sy index e007eec51..7e0a75197 100644 --- a/test/regress/cli/regress1/sygus/eval-uc.sy +++ b/test/regress/cli/regress1/sygus/eval-uc.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic HO_ALL) (declare-sort S 0) diff --git a/test/regress/cli/regress1/sygus/extract.sy b/test/regress/cli/regress1/sygus/extract.sy index fef48f364..3eb30462c 100644 --- a/test/regress/cli/regress1/sygus/extract.sy +++ b/test/regress/cli/regress1/sygus/extract.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/fast-enum-backtrack.sy b/test/regress/cli/regress1/sygus/fast-enum-backtrack.sy index 1778f91c7..2fc0a38c0 100644 --- a/test/regress/cli/regress1/sygus/fast-enum-backtrack.sy +++ b/test/regress/cli/regress1/sygus/fast-enum-backtrack.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-enum=fast (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/fg_polynomial3.sy b/test/regress/cli/regress1/sygus/fg_polynomial3.sy index 2da3809a8..d2e3c549f 100644 --- a/test/regress/cli/regress1/sygus/fg_polynomial3.sy +++ b/test/regress/cli/regress1/sygus/fg_polynomial3.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy b/test/regress/cli/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy index 18a1426d5..e78bcc89d 100644 --- a/test/regress/cli/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy +++ b/test/regress/cli/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/find_sc_bvult_bvnot.sy b/test/regress/cli/regress1/sygus/find_sc_bvult_bvnot.sy index 145064141..67dd69d5e 100644 --- a/test/regress/cli/regress1/sygus/find_sc_bvult_bvnot.sy +++ b/test/regress/cli/regress1/sygus/find_sc_bvult_bvnot.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegis-sample=trust --no-check-synth-sol (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/ground-ite-free-constant-si.sy b/test/regress/cli/regress1/sygus/ground-ite-free-constant-si.sy index 1d7241399..f7b1d2b90 100644 --- a/test/regress/cli/regress1/sygus/ground-ite-free-constant-si.sy +++ b/test/regress/cli/regress1/sygus/ground-ite-free-constant-si.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/hd-01-d1-prog.sy b/test/regress/cli/regress1/sygus/hd-01-d1-prog.sy index 9a28d6d79..3a09b9be4 100644 --- a/test/regress/cli/regress1/sygus/hd-01-d1-prog.sy +++ b/test/regress/cli/regress1/sygus/hd-01-d1-prog.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/cli/regress1/sygus/hd-19-d1-prog-dup-op.sy index ab8852d2e..43042ce87 100644 --- a/test/regress/cli/regress1/sygus/hd-19-d1-prog-dup-op.sy +++ b/test/regress/cli/regress1/sygus/hd-19-d1-prog-dup-op.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/hd-sdiv.sy b/test/regress/cli/regress1/sygus/hd-sdiv.sy index 2fdfb1c43..60120ea8a 100644 --- a/test/regress/cli/regress1/sygus/hd-sdiv.sy +++ b/test/regress/cli/regress1/sygus/hd-sdiv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/ho-sygus.sy b/test/regress/cli/regress1/sygus/ho-sygus.sy index d46d8ecde..afabc5d5e 100644 --- a/test/regress/cli/regress1/sygus/ho-sygus.sy +++ b/test/regress/cli/regress1/sygus/ho-sygus.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic HO_ALL) (synth-fun f ((y (-> Int Int)) (z Int)) Int) diff --git a/test/regress/cli/regress1/sygus/icfp_14.12-flip-args.sy b/test/regress/cli/regress1/sygus/icfp_14.12-flip-args.sy index 96851045c..a7d703415 100644 --- a/test/regress/cli/regress1/sygus/icfp_14.12-flip-args.sy +++ b/test/regress/cli/regress1/sygus/icfp_14.12-flip-args.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/icfp_14.12.sy b/test/regress/cli/regress1/sygus/icfp_14.12.sy index 6f76346d5..8f6979cc9 100644 --- a/test/regress/cli/regress1/sygus/icfp_14.12.sy +++ b/test/regress/cli/regress1/sygus/icfp_14.12.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/icfp_14_12_diff_types.sy b/test/regress/cli/regress1/sygus/icfp_14_12_diff_types.sy index 212943cab..12d098747 100644 --- a/test/regress/cli/regress1/sygus/icfp_14_12_diff_types.sy +++ b/test/regress/cli/regress1/sygus/icfp_14_12_diff_types.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/icfp_28_10.sy b/test/regress/cli/regress1/sygus/icfp_28_10.sy index 4ca73b87f..c853d2f44 100644 --- a/test/regress/cli/regress1/sygus/icfp_28_10.sy +++ b/test/regress/cli/regress1/sygus/icfp_28_10.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/icfp_easy-ite.sy b/test/regress/cli/regress1/sygus/icfp_easy-ite.sy index 63cc4736c..3f8a50e52 100644 --- a/test/regress/cli/regress1/sygus/icfp_easy-ite.sy +++ b/test/regress/cli/regress1/sygus/icfp_easy-ite.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/incremental-stream-ex.sy b/test/regress/cli/regress1/sygus/incremental-stream-ex.sy index 127a2e3bc..719f1a555 100644 --- a/test/regress/cli/regress1/sygus/incremental-stream-ex.sy +++ b/test/regress/cli/regress1/sygus/incremental-stream-ex.sy @@ -1,8 +1,8 @@ ; COMMAND-LINE: -i --sygus-out=status -;EXPECT: unsat -;EXPECT: unsat -;EXPECT: unsat -;EXPECT: unsat +;EXPECT: feasible +;EXPECT: feasible +;EXPECT: feasible +;EXPECT: feasible (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/int-any-const.sy b/test/regress/cli/regress1/sygus/int-any-const.sy index f377b23c1..3c033fe60 100644 --- a/test/regress/cli/regress1/sygus/int-any-const.sy +++ b/test/regress/cli/regress1/sygus/int-any-const.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/inv-example.sy b/test/regress/cli/regress1/sygus/inv-example.sy index bcc6c0aa8..059541aa3 100644 --- a/test/regress/cli/regress1/sygus/inv-example.sy +++ b/test/regress/cli/regress1/sygus/inv-example.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) diff --git a/test/regress/cli/regress1/sygus/inv-missed-sol-true.sy b/test/regress/cli/regress1/sygus/inv-missed-sol-true.sy index f8a3136f2..2d144e7c1 100644 --- a/test/regress/cli/regress1/sygus/inv-missed-sol-true.sy +++ b/test/regress/cli/regress1/sygus/inv-missed-sol-true.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/inv-unused.sy b/test/regress/cli/regress1/sygus/inv-unused.sy index a5eb41b26..24221814f 100644 --- a/test/regress/cli/regress1/sygus/inv-unused.sy +++ b/test/regress/cli/regress1/sygus/inv-unused.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) diff --git a/test/regress/cli/regress1/sygus/inv_gen_fig8.sy b/test/regress/cli/regress1/sygus/inv_gen_fig8.sy index 5c1aa4852..9e9a93c22 100644 --- a/test/regress/cli/regress1/sygus/inv_gen_fig8.sy +++ b/test/regress/cli/regress1/sygus/inv_gen_fig8.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun inv ((l Int)) Bool diff --git a/test/regress/cli/regress1/sygus/issue2914.sy b/test/regress/cli/regress1/sygus/issue2914.sy index 71a5a5987..13f382141 100644 --- a/test/regress/cli/regress1/sygus/issue2914.sy +++ b/test/regress/cli/regress1/sygus/issue2914.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/issue2935.sy b/test/regress/cli/regress1/sygus/issue2935.sy index ea8011a5e..c0323cb40 100644 --- a/test/regress/cli/regress1/sygus/issue2935.sy +++ b/test/regress/cli/regress1/sygus/issue2935.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/issue3109-share-sel.sy b/test/regress/cli/regress1/sygus/issue3109-share-sel.sy index 4b08a937d..60e8cea29 100644 --- a/test/regress/cli/regress1/sygus/issue3109-share-sel.sy +++ b/test/regress/cli/regress1/sygus/issue3109-share-sel.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/issue3320-quant.sy b/test/regress/cli/regress1/sygus/issue3320-quant.sy index 2d99ba5cf..255065499 100644 --- a/test/regress/cli/regress1/sygus/issue3320-quant.sy +++ b/test/regress/cli/regress1/sygus/issue3320-quant.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (declare-var x Int) diff --git a/test/regress/cli/regress1/sygus/issue3461.sy b/test/regress/cli/regress1/sygus/issue3461.sy index ebd6dd346..4ac8ed808 100644 --- a/test/regress/cli/regress1/sygus/issue3461.sy +++ b/test/regress/cli/regress1/sygus/issue3461.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/issue3580.sy b/test/regress/cli/regress1/sygus/issue3580.sy index 0366436b2..a40df6cee 100644 --- a/test/regress/cli/regress1/sygus/issue3580.sy +++ b/test/regress/cli/regress1/sygus/issue3580.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --sygus-enum=smart --lang=sygus2 (set-logic ALL) (synth-fun f diff --git a/test/regress/cli/regress1/sygus/issue3649.sy b/test/regress/cli/regress1/sygus/issue3649.sy index 0f7fc668c..661404616 100644 --- a/test/regress/cli/regress1/sygus/issue3649.sy +++ b/test/regress/cli/regress1/sygus/issue3649.sy @@ -1,4 +1,4 @@ -; EXPECT: unknown +; EXPECT: fail ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -q (set-logic ALL) (synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool) diff --git a/test/regress/cli/regress1/sygus/issue3802-default-consts.sy b/test/regress/cli/regress1/sygus/issue3802-default-consts.sy index e07365052..e4e5c5366 100644 --- a/test/regress/cli/regress1/sygus/issue3802-default-consts.sy +++ b/test/regress/cli/regress1/sygus/issue3802-default-consts.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic ALL) (synth-fun f diff --git a/test/regress/cli/regress1/sygus/large-const-simp.sy b/test/regress/cli/regress1/sygus/large-const-simp.sy index 08f280a4b..30f215090 100644 --- a/test/regress/cli/regress1/sygus/large-const-simp.sy +++ b/test/regress/cli/regress1/sygus/large-const-simp.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-add-const-grammar (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/let-bug-simp.sy b/test/regress/cli/regress1/sygus/let-bug-simp.sy index 1f383ab43..7ab34c4cf 100644 --- a/test/regress/cli/regress1/sygus/let-bug-simp.sy +++ b/test/regress/cli/regress1/sygus/let-bug-simp.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool diff --git a/test/regress/cli/regress1/sygus/list-head-x.sy b/test/regress/cli/regress1/sygus/list-head-x.sy index f1c99a28f..e29012506 100644 --- a/test/regress/cli/regress1/sygus/list-head-x.sy +++ b/test/regress/cli/regress1/sygus/list-head-x.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/list_recursor.sy b/test/regress/cli/regress1/sygus/list_recursor.sy index cb1ae2721..041045ca1 100644 --- a/test/regress/cli/regress1/sygus/list_recursor.sy +++ b/test/regress/cli/regress1/sygus/list_recursor.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic HO_ALL) diff --git a/test/regress/cli/regress1/sygus/logiccell_help.sy b/test/regress/cli/regress1/sygus/logiccell_help.sy index d6e8a75a4..cd47df17a 100644 --- a/test/regress/cli/regress1/sygus/logiccell_help.sy +++ b/test/regress/cli/regress1/sygus/logiccell_help.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/max-all.sy b/test/regress/cli/regress1/sygus/max-all.sy index aaf0e3bf0..f63d8d737 100644 --- a/test/regress/cli/regress1/sygus/max-all.sy +++ b/test/regress/cli/regress1/sygus/max-all.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-si-rcons-limit=0 --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/max-limit.sy b/test/regress/cli/regress1/sygus/max-limit.sy index 3031c869b..40790f36d 100644 --- a/test/regress/cli/regress1/sygus/max-limit.sy +++ b/test/regress/cli/regress1/sygus/max-limit.sy @@ -1,7 +1,7 @@ ; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=all-limit --sygus-si-rcons-limit=0 --sygus-out=status ; ERROR-SCRUBBER: grep -o "reconstruction to syntax failed." ; EXPECT-ERROR: reconstruction to syntax failed. -; EXPECT: unknown +; EXPECT: fail ; REQUIRES: no-competition (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/max-try1.sy b/test/regress/cli/regress1/sygus/max-try1.sy index 8c1153ba0..62c031c65 100644 --- a/test/regress/cli/regress1/sygus/max-try1.sy +++ b/test/regress/cli/regress1/sygus/max-try1.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=try --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/max-try2.sy b/test/regress/cli/regress1/sygus/max-try2.sy index ef8df46de..64f96a66b 100644 --- a/test/regress/cli/regress1/sygus/max-try2.sy +++ b/test/regress/cli/regress1/sygus/max-try2.sy @@ -1,7 +1,7 @@ ; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=try --sygus-out=status ; ERROR-SCRUBBER: grep -o "reconstruction to syntax failed." ; EXPECT-ERROR: reconstruction to syntax failed. -; EXPECT: unknown +; EXPECT: fail ; REQUIRES: no-competition (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/max.sy b/test/regress/cli/regress1/sygus/max.sy index e753277cc..da267a74a 100644 --- a/test/regress/cli/regress1/sygus/max.sy +++ b/test/regress/cli/regress1/sygus/max.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/max2-bv.sy b/test/regress/cli/regress1/sygus/max2-bv.sy index b8a23aba5..2fc371572 100644 --- a/test/regress/cli/regress1/sygus/max2-bv.sy +++ b/test/regress/cli/regress1/sygus/max2-bv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-bv (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/multi-fun-polynomial2.sy b/test/regress/cli/regress1/sygus/multi-fun-polynomial2.sy index a20bf853d..9a20ec149 100644 --- a/test/regress/cli/regress1/sygus/multi-fun-polynomial2.sy +++ b/test/regress/cli/regress1/sygus/multi-fun-polynomial2.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/nflat-fwd-3.sy b/test/regress/cli/regress1/sygus/nflat-fwd-3.sy index f9b6708d5..c7dee7dd1 100644 --- a/test/regress/cli/regress1/sygus/nflat-fwd-3.sy +++ b/test/regress/cli/regress1/sygus/nflat-fwd-3.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int diff --git a/test/regress/cli/regress1/sygus/nflat-fwd.sy b/test/regress/cli/regress1/sygus/nflat-fwd.sy index c36232a5d..20310a9fa 100644 --- a/test/regress/cli/regress1/sygus/nflat-fwd.sy +++ b/test/regress/cli/regress1/sygus/nflat-fwd.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int diff --git a/test/regress/cli/regress1/sygus/nia-max-square-ns.sy b/test/regress/cli/regress1/sygus/nia-max-square-ns.sy index 1177be5e7..39f217529 100644 --- a/test/regress/cli/regress1/sygus/nia-max-square-ns.sy +++ b/test/regress/cli/regress1/sygus/nia-max-square-ns.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --nl-ext-tplanes (set-logic NIA) diff --git a/test/regress/cli/regress1/sygus/no-flat-simp.sy b/test/regress/cli/regress1/sygus/no-flat-simp.sy index 42b73394b..e0e30254e 100644 --- a/test/regress/cli/regress1/sygus/no-flat-simp.sy +++ b/test/regress/cli/regress1/sygus/no-flat-simp.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/no-mention.sy b/test/regress/cli/regress1/sygus/no-mention.sy index ff10c1263..fe1c21e42 100644 --- a/test/regress/cli/regress1/sygus/no-mention.sy +++ b/test/regress/cli/regress1/sygus/no-mention.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/node-discrete.sy b/test/regress/cli/regress1/sygus/node-discrete.sy index 35d00b0a5..4b84657da 100644 --- a/test/regress/cli/regress1/sygus/node-discrete.sy +++ b/test/regress/cli/regress1/sygus/node-discrete.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol (set-logic ALL) @@ -22,7 +22,7 @@ ; reliability (define-fun rel () Real 0.7) -; new chance of success +; new chance of feasible (define-fun updateReal ((addP Real) (currP Real)) Real (+ currP (* (- 1.0 currP) addP)) ) @@ -105,7 +105,7 @@ (let ((dst_pair (mkPair dst pck))) (let ((src_pair (mkPair actor pck))) (let ((chSuccess (ite (select prevRcv src_pair) rel 0.0))) - ; success and failure + ; feasible and failure (appendStateToPState (mkState (store prevRcv dst_pair true)) (* r chSuccess) @@ -121,7 +121,7 @@ (let ((dst_pair (mkPair actor pck))) (let ((src_pair (mkPair src pck))) (let ((chSuccess (ite (select prevRcv src_pair) rel 0.0))) - ; success and failure + ; feasible and failure (appendStateToPState (mkState (store prevRcv dst_pair true)) (* r chSuccess) diff --git a/test/regress/cli/regress1/sygus/once_2.sy b/test/regress/cli/regress1/sygus/once_2.sy index af6d56aaf..7add2784d 100644 --- a/test/regress/cli/regress1/sygus/once_2.sy +++ b/test/regress/cli/regress1/sygus/once_2.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/only-const-grammar.sy b/test/regress/cli/regress1/sygus/only-const-grammar.sy index 25effd154..bd21bcecc 100644 --- a/test/regress/cli/regress1/sygus/only-const-grammar.sy +++ b/test/regress/cli/regress1/sygus/only-const-grammar.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/pLTL_5_trace.sy b/test/regress/cli/regress1/sygus/pLTL_5_trace.sy index 532a8f3a8..c4c3f6062 100644 --- a/test/regress/cli/regress1/sygus/pLTL_5_trace.sy +++ b/test/regress/cli/regress1/sygus/pLTL_5_trace.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/parity-si-rcons.sy b/test/regress/cli/regress1/sygus/parity-si-rcons.sy index 16ade4ee5..8dd090ab6 100644 --- a/test/regress/cli/regress1/sygus/parity-si-rcons.sy +++ b/test/regress/cli/regress1/sygus/parity-si-rcons.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --sygus-si-rcons=try --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/pbe_multi.sy b/test/regress/cli/regress1/sygus/pbe_multi.sy index 4c588ee17..23aab101e 100644 --- a/test/regress/cli/regress1/sygus/pbe_multi.sy +++ b/test/regress/cli/regress1/sygus/pbe_multi.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/phone-1-long.sy b/test/regress/cli/regress1/sygus/phone-1-long.sy index 6d89a4e6c..40e4a3496 100644 --- a/test/regress/cli/regress1/sygus/phone-1-long.sy +++ b/test/regress/cli/regress1/sygus/phone-1-long.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-fair=direct -; EXPECT: unsat +; EXPECT: feasible (set-logic SLIA) (synth-fun f ((name String)) String diff --git a/test/regress/cli/regress1/sygus/planning-unif.sy b/test/regress/cli/regress1/sygus/planning-unif.sy index 212c25595..b13003663 100644 --- a/test/regress/cli/regress1/sygus/planning-unif.sy +++ b/test/regress/cli/regress1/sygus/planning-unif.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/process-10-vars.sy b/test/regress/cli/regress1/sygus/process-10-vars.sy index 86fac86cd..d2c95cc33 100644 --- a/test/regress/cli/regress1/sygus/process-10-vars.sy +++ b/test/regress/cli/regress1/sygus/process-10-vars.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-arg-relevant -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) (synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) diff --git a/test/regress/cli/regress1/sygus/qe.sy b/test/regress/cli/regress1/sygus/qe.sy index eba30350d..ebe4ac5a1 100644 --- a/test/regress/cli/regress1/sygus/qe.sy +++ b/test/regress/cli/regress1/sygus/qe.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-qe-preproc (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/rand_const.sy b/test/regress/cli/regress1/sygus/rand_const.sy index cc87af3fe..442c62224 100644 --- a/test/regress/cli/regress1/sygus/rand_const.sy +++ b/test/regress/cli/regress1/sygus/rand_const.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-enum=random --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic BV) diff --git a/test/regress/cli/regress1/sygus/rand_p_0.sy b/test/regress/cli/regress1/sygus/rand_p_0.sy index 03d6cbc67..6850afac3 100644 --- a/test/regress/cli/regress1/sygus/rand_p_0.sy +++ b/test/regress/cli/regress1/sygus/rand_p_0.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-enum=random --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic BV) (set-option :sygus-enum-random-p 0) diff --git a/test/regress/cli/regress1/sygus/rand_p_1.sy b/test/regress/cli/regress1/sygus/rand_p_1.sy index a1eb85183..2501568a9 100644 --- a/test/regress/cli/regress1/sygus/rand_p_1.sy +++ b/test/regress/cli/regress1/sygus/rand_p_1.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-enum=random --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic BV) (set-option :sygus-enum-random-p 1) diff --git a/test/regress/cli/regress1/sygus/re-concat.sy b/test/regress/cli/regress1/sygus/re-concat.sy index ac1172e33..cbd07525a 100644 --- a/test/regress/cli/regress1/sygus/re-concat.sy +++ b/test/regress/cli/regress1/sygus/re-concat.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun f () RegLan ((Start RegLan) (Tokens String)) ( diff --git a/test/regress/cli/regress1/sygus/real-any-const.sy b/test/regress/cli/regress1/sygus/real-any-const.sy index 53db26910..93bd36bd6 100644 --- a/test/regress/cli/regress1/sygus/real-any-const.sy +++ b/test/regress/cli/regress1/sygus/real-any-const.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise (set-logic LRA) diff --git a/test/regress/cli/regress1/sygus/real-grammar.sy b/test/regress/cli/regress1/sygus/real-grammar.sy index d664bf2a2..6af5689db 100644 --- a/test/regress/cli/regress1/sygus/real-grammar.sy +++ b/test/regress/cli/regress1/sygus/real-grammar.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none (set-logic LRA) diff --git a/test/regress/cli/regress1/sygus/rec-fun-swap.sy b/test/regress/cli/regress1/sygus/rec-fun-swap.sy index 056d6a8fc..0d19d297d 100644 --- a/test/regress/cli/regress1/sygus/rec-fun-swap.sy +++ b/test/regress/cli/regress1/sygus/rec-fun-swap.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/rec-fun-sygus.sy b/test/regress/cli/regress1/sygus/rec-fun-sygus.sy index 769e173de..282a6c853 100644 --- a/test/regress/cli/regress1/sygus/rec-fun-sygus.sy +++ b/test/regress/cli/regress1/sygus/rec-fun-sygus.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/rec-fun-while-1.sy b/test/regress/cli/regress1/sygus/rec-fun-while-1.sy index e805fdc20..3a362bf1f 100644 --- a/test/regress/cli/regress1/sygus/rec-fun-while-1.sy +++ b/test/regress/cli/regress1/sygus/rec-fun-while-1.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/rec-fun-while-2.sy b/test/regress/cli/regress1/sygus/rec-fun-while-2.sy index 7e32384b3..ba7d7f832 100644 --- a/test/regress/cli/regress1/sygus/rec-fun-while-2.sy +++ b/test/regress/cli/regress1/sygus/rec-fun-while-2.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/rec-fun-while-infinite.sy b/test/regress/cli/regress1/sygus/rec-fun-while-infinite.sy index b43b3d5e2..ed2dd87a3 100644 --- a/test/regress/cli/regress1/sygus/rec-fun-while-infinite.sy +++ b/test/regress/cli/regress1/sygus/rec-fun-while-infinite.sy @@ -1,4 +1,4 @@ -; EXPECT: unknown +; EXPECT: fail ; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/repair-const-rl.sy b/test/regress/cli/regress1/sygus/repair-const-rl.sy index 3374d6a8a..7688681f9 100644 --- a/test/regress/cli/regress1/sygus/repair-const-rl.sy +++ b/test/regress/cli/regress1/sygus/repair-const-rl.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --sygus-si=none --sygus-repair-const --lang=sygus2 (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/replicate-mod-assume.sy b/test/regress/cli/regress1/sygus/replicate-mod-assume.sy index c10cab2f5..c7c9131af 100644 --- a/test/regress/cli/regress1/sygus/replicate-mod-assume.sy +++ b/test/regress/cli/regress1/sygus/replicate-mod-assume.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun fr0 ((_v Int) (n Int) (x Int)) Int diff --git a/test/regress/cli/regress1/sygus/replicate-mod.sy b/test/regress/cli/regress1/sygus/replicate-mod.sy index fbe3b7d65..01c49d752 100644 --- a/test/regress/cli/regress1/sygus/replicate-mod.sy +++ b/test/regress/cli/regress1/sygus/replicate-mod.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-qe-preproc --sygus-si=all --sygus-out=status (set-logic LIA) (synth-fun fr0 ((_v Int) (n Int) (x Int)) Int diff --git a/test/regress/cli/regress1/sygus/rex-strings-alarm.sy b/test/regress/cli/regress1/sygus/rex-strings-alarm.sy index aa2ddb2a3..25854886f 100644 --- a/test/regress/cli/regress1/sygus/rex-strings-alarm.sy +++ b/test/regress/cli/regress1/sygus/rex-strings-alarm.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 --strings-exp (set-logic S) diff --git a/test/regress/cli/regress1/sygus/sets-pred-test.sy b/test/regress/cli/regress1/sygus/sets-pred-test.sy index 18e783027..2c9524ef2 100644 --- a/test/regress/cli/regress1/sygus/sets-pred-test.sy +++ b/test/regress/cli/regress1/sygus/sets-pred-test.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (synth-fun P ((x (Set Int))) Bool) diff --git a/test/regress/cli/regress1/sygus/simple-no-rewrite.sy b/test/regress/cli/regress1/sygus/simple-no-rewrite.sy index 68e8a3a48..bb3c4fc54 100644 --- a/test/regress/cli/regress1/sygus/simple-no-rewrite.sy +++ b/test/regress/cli/regress1/sygus/simple-no-rewrite.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic UF) diff --git a/test/regress/cli/regress1/sygus/simple-not-in-grammar.sy b/test/regress/cli/regress1/sygus/simple-not-in-grammar.sy index f9f6354f5..365c0927f 100644 --- a/test/regress/cli/regress1/sygus/simple-not-in-grammar.sy +++ b/test/regress/cli/regress1/sygus/simple-not-in-grammar.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic UF) diff --git a/test/regress/cli/regress1/sygus/simple-regexp.sy b/test/regress/cli/regress1/sygus/simple-regexp.sy index b7646725d..118cb9a85 100644 --- a/test/regress/cli/regress1/sygus/simple-regexp.sy +++ b/test/regress/cli/regress1/sygus/simple-regexp.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun P ((x String)) Bool diff --git a/test/regress/cli/regress1/sygus/simple-rewrite-in-db.sy b/test/regress/cli/regress1/sygus/simple-rewrite-in-db.sy index 46d3b59b0..8fcd9aa89 100644 --- a/test/regress/cli/regress1/sygus/simple-rewrite-in-db.sy +++ b/test/regress/cli/regress1/sygus/simple-rewrite-in-db.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic UF) diff --git a/test/regress/cli/regress1/sygus/simple-rewrite-not-in-db.sy b/test/regress/cli/regress1/sygus/simple-rewrite-not-in-db.sy index 5b4dbbee1..98c851099 100644 --- a/test/regress/cli/regress1/sygus/simple-rewrite-not-in-db.sy +++ b/test/regress/cli/regress1/sygus/simple-rewrite-not-in-db.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-si=all --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic UF) diff --git a/test/regress/cli/regress1/sygus/stopwatch-bt.sy b/test/regress/cli/regress1/sygus/stopwatch-bt.sy index c33e16bcd..6044cbccb 100644 --- a/test/regress/cli/regress1/sygus/stopwatch-bt.sy +++ b/test/regress/cli/regress1/sygus/stopwatch-bt.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=post --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/strings-any-term1.sy b/test/regress/cli/regress1/sygus/strings-any-term1.sy index 2c3eaac33..50bb17817 100644 --- a/test/regress/cli/regress1/sygus/strings-any-term1.sy +++ b/test/regress/cli/regress1/sygus/strings-any-term1.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term (set-logic ALL) (synth-fun f ((x String) (y String)) Int) diff --git a/test/regress/cli/regress1/sygus/strings-concat-3-args.sy b/test/regress/cli/regress1/sygus/strings-concat-3-args.sy index 681d3ccff..3821e343e 100644 --- a/test/regress/cli/regress1/sygus/strings-concat-3-args.sy +++ b/test/regress/cli/regress1/sygus/strings-concat-3-args.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun f ((x String)) String diff --git a/test/regress/cli/regress1/sygus/strings-double-rec.sy b/test/regress/cli/regress1/sygus/strings-double-rec.sy index 0c21015e7..333f20fab 100644 --- a/test/regress/cli/regress1/sygus/strings-double-rec.sy +++ b/test/regress/cli/regress1/sygus/strings-double-rec.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/strings-no-syntax.sy b/test/regress/cli/regress1/sygus/strings-no-syntax.sy index 8abb33f33..1805df168 100644 --- a/test/regress/cli/regress1/sygus/strings-no-syntax.sy +++ b/test/regress/cli/regress1/sygus/strings-no-syntax.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/strings-small.sy b/test/regress/cli/regress1/sygus/strings-small.sy index 834898b02..2c79cadd6 100644 --- a/test/regress/cli/regress1/sygus/strings-small.sy +++ b/test/regress/cli/regress1/sygus/strings-small.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun f ((firstname String) (lastname String)) String diff --git a/test/regress/cli/regress1/sygus/strings-template-infer-unused.sy b/test/regress/cli/regress1/sygus/strings-template-infer-unused.sy index 2c075388a..0066b7b69 100644 --- a/test/regress/cli/regress1/sygus/strings-template-infer-unused.sy +++ b/test/regress/cli/regress1/sygus/strings-template-infer-unused.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/strings-template-infer.sy b/test/regress/cli/regress1/sygus/strings-template-infer.sy index 8cbce19b6..909a887e4 100644 --- a/test/regress/cli/regress1/sygus/strings-template-infer.sy +++ b/test/regress/cli/regress1/sygus/strings-template-infer.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/strings-trivial-simp.sy b/test/regress/cli/regress1/sygus/strings-trivial-simp.sy index c0e3f0ea6..322403070 100644 --- a/test/regress/cli/regress1/sygus/strings-trivial-simp.sy +++ b/test/regress/cli/regress1/sygus/strings-trivial-simp.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/strings-trivial-two-type.sy b/test/regress/cli/regress1/sygus/strings-trivial-two-type.sy index ba9ac5064..89fd5d424 100644 --- a/test/regress/cli/regress1/sygus/strings-trivial-two-type.sy +++ b/test/regress/cli/regress1/sygus/strings-trivial-two-type.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/strings-trivial.sy b/test/regress/cli/regress1/sygus/strings-trivial.sy index 7fe96cf14..3823e6cab 100644 --- a/test/regress/cli/regress1/sygus/strings-trivial.sy +++ b/test/regress/cli/regress1/sygus/strings-trivial.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress1/sygus/sygus-dt.sy b/test/regress/cli/regress1/sygus/sygus-dt.sy index 7539fdd0d..ecf7d86e1 100644 --- a/test/regress/cli/regress1/sygus/sygus-dt.sy +++ b/test/regress/cli/regress1/sygus/sygus-dt.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/sygus-lambda-fv.sy b/test/regress/cli/regress1/sygus/sygus-lambda-fv.sy index d96960c83..9bcb9e774 100644 --- a/test/regress/cli/regress1/sygus/sygus-lambda-fv.sy +++ b/test/regress/cli/regress1/sygus/sygus-lambda-fv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/sygus-uf-ex.sy b/test/regress/cli/regress1/sygus/sygus-uf-ex.sy index c74ce79b7..acf14ccae 100644 --- a/test/regress/cli/regress1/sygus/sygus-uf-ex.sy +++ b/test/regress/cli/regress1/sygus/sygus-uf-ex.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic HO_ALL) diff --git a/test/regress/cli/regress1/sygus/t8.sy b/test/regress/cli/regress1/sygus/t8.sy index 6ac904832..fac55d9cb 100644 --- a/test/regress/cli/regress1/sygus/t8.sy +++ b/test/regress/cli/regress1/sygus/t8.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) ( diff --git a/test/regress/cli/regress1/sygus/temp_input_to_synth_ic-error-121418.sy b/test/regress/cli/regress1/sygus/temp_input_to_synth_ic-error-121418.sy index 385ade07f..10164d48f 100644 --- a/test/regress/cli/regress1/sygus/temp_input_to_synth_ic-error-121418.sy +++ b/test/regress/cli/regress1/sygus/temp_input_to_synth_ic-error-121418.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (define-sort FP () (_ FloatingPoint 3 5)) diff --git a/test/regress/cli/regress1/sygus/tester.sy b/test/regress/cli/regress1/sygus/tester.sy index c5b72b009..d2c5f6773 100644 --- a/test/regress/cli/regress1/sygus/tester.sy +++ b/test/regress/cli/regress1/sygus/tester.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic DTSLIA) diff --git a/test/regress/cli/regress1/sygus/tl-type-0.sy b/test/regress/cli/regress1/sygus/tl-type-0.sy index 3da21f6dc..704f8a143 100644 --- a/test/regress/cli/regress1/sygus/tl-type-0.sy +++ b/test/regress/cli/regress1/sygus/tl-type-0.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int diff --git a/test/regress/cli/regress1/sygus/tl-type-4x.sy b/test/regress/cli/regress1/sygus/tl-type-4x.sy index 7d6fa778e..1892885ae 100644 --- a/test/regress/cli/regress1/sygus/tl-type-4x.sy +++ b/test/regress/cli/regress1/sygus/tl-type-4x.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int diff --git a/test/regress/cli/regress1/sygus/tl-type.sy b/test/regress/cli/regress1/sygus/tl-type.sy index 8be604b23..a5e7a4252 100644 --- a/test/regress/cli/regress1/sygus/tl-type.sy +++ b/test/regress/cli/regress1/sygus/tl-type.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int diff --git a/test/regress/cli/regress1/sygus/triv-type-mismatch-si.sy b/test/regress/cli/regress1/sygus/triv-type-mismatch-si.sy index 6ef891560..875ff3b20 100644 --- a/test/regress/cli/regress1/sygus/triv-type-mismatch-si.sy +++ b/test/regress/cli/regress1/sygus/triv-type-mismatch-si.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/twolets1.sy b/test/regress/cli/regress1/sygus/twolets1.sy index 7f3fed923..b94d4390e 100644 --- a/test/regress/cli/regress1/sygus/twolets1.sy +++ b/test/regress/cli/regress1/sygus/twolets1.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/twolets2-orig.sy b/test/regress/cli/regress1/sygus/twolets2-orig.sy index 16b3e27aa..9da634005 100644 --- a/test/regress/cli/regress1/sygus/twolets2-orig.sy +++ b/test/regress/cli/regress1/sygus/twolets2-orig.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) (define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) diff --git a/test/regress/cli/regress1/sygus/unbdd_inv_gen_winf1.sy b/test/regress/cli/regress1/sygus/unbdd_inv_gen_winf1.sy index edfc2176b..a39dae89b 100644 --- a/test/regress/cli/regress1/sygus/unbdd_inv_gen_winf1.sy +++ b/test/regress/cli/regress1/sygus/unbdd_inv_gen_winf1.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress1/sygus/univ_2-long-repeat.sy b/test/regress/cli/regress1/sygus/univ_2-long-repeat.sy index a2c4c028d..fd34d5bea 100644 --- a/test/regress/cli/regress1/sygus/univ_2-long-repeat.sy +++ b/test/regress/cli/regress1/sygus/univ_2-long-repeat.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-fair=direct --sygus-out=status (set-logic SLIA) diff --git a/test/regress/cli/regress2/sygus/MPwL_d1s3.sy b/test/regress/cli/regress2/sygus/MPwL_d1s3.sy index 9ff13d5ab..0e5b03efc 100644 --- a/test/regress/cli/regress2/sygus/MPwL_d1s3.sy +++ b/test/regress/cli/regress2/sygus/MPwL_d1s3.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress2/sygus/array_sum_dd.sy b/test/regress/cli/regress2/sygus/array_sum_dd.sy index 2b4177843..dea7d8f9c 100644 --- a/test/regress/cli/regress2/sygus/array_sum_dd.sy +++ b/test/regress/cli/regress2/sygus/array_sum_dd.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun findSum ((y1 Int) (y2 Int)) Int ((Start Int) (BoolExpr Bool)) ( diff --git a/test/regress/cli/regress2/sygus/cegisunif-depth1-bv.sy b/test/regress/cli/regress2/sygus/cegisunif-depth1-bv.sy index 6aa17ef30..286fd13b3 100644 --- a/test/regress/cli/regress2/sygus/cegisunif-depth1-bv.sy +++ b/test/regress/cli/regress2/sygus/cegisunif-depth1-bv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress2/sygus/ex23.sy b/test/regress/cli/regress2/sygus/ex23.sy index 9e3d2ea75..9a0c7055b 100644 --- a/test/regress/cli/regress2/sygus/ex23.sy +++ b/test/regress/cli/regress2/sygus/ex23.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const (set-logic LIA) diff --git a/test/regress/cli/regress2/sygus/examples-deq.sy b/test/regress/cli/regress2/sygus/examples-deq.sy index 5b52e1da7..5e5a45f7b 100644 --- a/test/regress/cli/regress2/sygus/examples-deq.sy +++ b/test/regress/cli/regress2/sygus/examples-deq.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int) diff --git a/test/regress/cli/regress2/sygus/icfp_easy_mt_ite.sy b/test/regress/cli/regress2/sygus/icfp_easy_mt_ite.sy index d7cc161da..bc1286e76 100644 --- a/test/regress/cli/regress2/sygus/icfp_easy_mt_ite.sy +++ b/test/regress/cli/regress2/sygus/icfp_easy_mt_ite.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) diff --git a/test/regress/cli/regress2/sygus/lustre-real.sy b/test/regress/cli/regress2/sygus/lustre-real.sy index b7637567f..cd5bb6244 100644 --- a/test/regress/cli/regress2/sygus/lustre-real.sy +++ b/test/regress/cli/regress2/sygus/lustre-real.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIRA) (define-fun diff --git a/test/regress/cli/regress2/sygus/max2-univ.sy b/test/regress/cli/regress2/sygus/max2-univ.sy index d8222ded2..e4abed5d1 100644 --- a/test/regress/cli/regress2/sygus/max2-univ.sy +++ b/test/regress/cli/regress2/sygus/max2-univ.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes) (set-logic LIA) diff --git a/test/regress/cli/regress2/sygus/min_IC_1.sy b/test/regress/cli/regress2/sygus/min_IC_1.sy index 8c0e2d82b..29df32707 100644 --- a/test/regress/cli/regress2/sygus/min_IC_1.sy +++ b/test/regress/cli/regress2/sygus/min_IC_1.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --fp-exp (set-logic ALL) (define-sort FP () (_ FloatingPoint 3 5)) diff --git a/test/regress/cli/regress2/sygus/mpg_guard1-dd.sy b/test/regress/cli/regress2/sygus/mpg_guard1-dd.sy index 98f13bb92..f3287ed52 100644 --- a/test/regress/cli/regress2/sygus/mpg_guard1-dd.sy +++ b/test/regress/cli/regress2/sygus/mpg_guard1-dd.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress2/sygus/multi-udiv.sy b/test/regress/cli/regress2/sygus/multi-udiv.sy index 3a81a4885..8b08aaf1b 100644 --- a/test/regress/cli/regress2/sygus/multi-udiv.sy +++ b/test/regress/cli/regress2/sygus/multi-udiv.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast (set-logic BV) diff --git a/test/regress/cli/regress2/sygus/no-bad-filter.sy b/test/regress/cli/regress2/sygus/no-bad-filter.sy index 4e7c35033..a3d7e28b4 100644 --- a/test/regress/cli/regress2/sygus/no-bad-filter.sy +++ b/test/regress/cli/regress2/sygus/no-bad-filter.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-out=status --sygus-si=all -; EXPECT: unsat +; EXPECT: feasible ; This regression ensures that we are not too aggressive in filtering ; enumerated shapes in the pool. diff --git a/test/regress/cli/regress2/sygus/no-syntax-test-no-si.sy b/test/regress/cli/regress2/sygus/no-syntax-test-no-si.sy index 1906e3ef1..4f5229a53 100644 --- a/test/regress/cli/regress2/sygus/no-syntax-test-no-si.sy +++ b/test/regress/cli/regress2/sygus/no-syntax-test-no-si.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress2/sygus/pbe_bvurem.sy b/test/regress/cli/regress2/sygus/pbe_bvurem.sy index 07f029577..89b065ac1 100644 --- a/test/regress/cli/regress2/sygus/pbe_bvurem.sy +++ b/test/regress/cli/regress2/sygus/pbe_bvurem.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) (define-sort BV () (_ BitVec 8)) diff --git a/test/regress/cli/regress2/sygus/process-10-vars-2fun.sy b/test/regress/cli/regress2/sygus/process-10-vars-2fun.sy index 00a0099b0..82d153b9f 100644 --- a/test/regress/cli/regress2/sygus/process-10-vars-2fun.sy +++ b/test/regress/cli/regress2/sygus/process-10-vars-2fun.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) (synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) diff --git a/test/regress/cli/regress2/sygus/process-arg-invariance.sy b/test/regress/cli/regress2/sygus/process-arg-invariance.sy index 15bffb073..2c86e7541 100644 --- a/test/regress/cli/regress2/sygus/process-arg-invariance.sy +++ b/test/regress/cli/regress2/sygus/process-arg-invariance.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant -; EXPECT: unsat +; EXPECT: feasible (set-logic LIA) (synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) diff --git a/test/regress/cli/regress2/sygus/proj-issue119.sy b/test/regress/cli/regress2/sygus/proj-issue119.sy index 910126e2e..a67f0671a 100644 --- a/test/regress/cli/regress2/sygus/proj-issue119.sy +++ b/test/regress/cli/regress2/sygus/proj-issue119.sy @@ -1,5 +1,5 @@ ; COMMAND-LINE: --sygus-out=status -; EXPECT: unsat +; EXPECT: feasible (set-logic ALL) (define-fun safe-mod ((x Int) (y Int)) Int (mod x (+ 1 (abs y)))) (synth-fun args_0_refinement_0 diff --git a/test/regress/cli/regress2/sygus/real-grammar-neg.sy b/test/regress/cli/regress2/sygus/real-grammar-neg.sy index d9a66bcce..7d1c35e3a 100644 --- a/test/regress/cli/regress2/sygus/real-grammar-neg.sy +++ b/test/regress/cli/regress2/sygus/real-grammar-neg.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --no-sygus-pbe (set-logic LRA) diff --git a/test/regress/cli/regress2/sygus/sets-fun-test.sy b/test/regress/cli/regress2/sygus/sets-fun-test.sy index 561014ed5..9a0149dd3 100644 --- a/test/regress/cli/regress2/sygus/sets-fun-test.sy +++ b/test/regress/cli/regress2/sygus/sets-fun-test.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast (set-logic ALL) (synth-fun f ((x Int)) (Set Int)) diff --git a/test/regress/cli/regress2/sygus/strings-no-syntax-len.sy b/test/regress/cli/regress2/sygus/strings-no-syntax-len.sy index e0b039c16..8312c4af5 100644 --- a/test/regress/cli/regress2/sygus/strings-no-syntax-len.sy +++ b/test/regress/cli/regress2/sygus/strings-no-syntax-len.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/cli/regress2/sygus/sumn_recur_synth.sy b/test/regress/cli/regress2/sygus/sumn_recur_synth.sy index 103992dfe..959c094ab 100644 --- a/test/regress/cli/regress2/sygus/sumn_recur_synth.sy +++ b/test/regress/cli/regress2/sygus/sumn_recur_synth.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic UFLIA) diff --git a/test/regress/cli/regress2/sygus/three.sy b/test/regress/cli/regress2/sygus/three.sy index 17af8c93b..402b8d358 100644 --- a/test/regress/cli/regress2/sygus/three.sy +++ b/test/regress/cli/regress2/sygus/three.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast (set-logic NIA) diff --git a/test/regress/cli/regress3/DRAGON_1.lus.sy b/test/regress/cli/regress3/DRAGON_1.lus.sy index 4d9510ade..baa97b0cc 100644 --- a/test/regress/cli/regress3/DRAGON_1.lus.sy +++ b/test/regress/cli/regress3/DRAGON_1.lus.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=complete --cegis-sample=use (set-logic LIA) diff --git a/test/regress/cli/regress3/cegisunif-depth1.sy b/test/regress/cli/regress3/cegisunif-depth1.sy index 06c4d3a78..ba1fb07c6 100644 --- a/test/regress/cli/regress3/cegisunif-depth1.sy +++ b/test/regress/cli/regress3/cegisunif-depth1.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status (set-logic LIA) diff --git a/test/regress/cli/regress3/inv_gen_n_c11.sy b/test/regress/cli/regress3/inv_gen_n_c11.sy index aebc03dea..a01e30725 100644 --- a/test/regress/cli/regress3/inv_gen_n_c11.sy +++ b/test/regress/cli/regress3/inv_gen_n_c11.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun inv ((i Int) (l Int)) Bool diff --git a/test/regress/cli/regress3/nia-max-square.sy b/test/regress/cli/regress3/nia-max-square.sy index 0657494b1..514709735 100644 --- a/test/regress/cli/regress3/nia-max-square.sy +++ b/test/regress/cli/regress3/nia-max-square.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --nl-ext-tplanes (set-logic NIA) diff --git a/test/regress/cli/regress3/policyM.sy b/test/regress/cli/regress3/policyM.sy index 0e9b33148..21c7622bf 100644 --- a/test/regress/cli/regress3/policyM.sy +++ b/test/regress/cli/regress3/policyM.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic ALL) diff --git a/test/regress/cli/regress3/sixfuncs.sy b/test/regress/cli/regress3/sixfuncs.sy index 89f112e0a..d8fe76505 100644 --- a/test/regress/cli/regress3/sixfuncs.sy +++ b/test/regress/cli/regress3/sixfuncs.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification (set-logic LIA) diff --git a/test/regress/cli/regress3/strings-any-term.sy b/test/regress/cli/regress3/strings-any-term.sy index d405d3b49..97c987529 100644 --- a/test/regress/cli/regress3/strings-any-term.sy +++ b/test/regress/cli/regress3/strings-any-term.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term --sygus-enum=smart (set-logic ALL) (synth-fun f ((x String) (y String)) Int) diff --git a/test/regress/cli/regress3/unbdd_inv_gen_ex7.sy b/test/regress/cli/regress3/unbdd_inv_gen_ex7.sy index 34abb6de8..ac866b052 100644 --- a/test/regress/cli/regress3/unbdd_inv_gen_ex7.sy +++ b/test/regress/cli/regress3/unbdd_inv_gen_ex7.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun inv ((i Int) (y Int) (l Int)) Bool diff --git a/test/regress/cli/regress3/unifpi-solve-car_1.lus.sy b/test/regress/cli/regress3/unifpi-solve-car_1.lus.sy index c1d196f60..e31234ed7 100644 --- a/test/regress/cli/regress3/unifpi-solve-car_1.lus.sy +++ b/test/regress/cli/regress3/unifpi-solve-car_1.lus.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete (set-logic LIA) diff --git a/test/regress/cli/regress3/vcb.sy b/test/regress/cli/regress3/vcb.sy index a0122193d..8ce9bdfca 100644 --- a/test/regress/cli/regress3/vcb.sy +++ b/test/regress/cli/regress3/vcb.sy @@ -1,4 +1,4 @@ -; EXPECT: unsat +; EXPECT: feasible ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-repair-const --decision=justification (set-logic LIA) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 7e9fd5880..c9b47e2de 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2679,7 +2679,8 @@ TEST_F(TestApiBlackSolver, getSynthSolution) ASSERT_THROW(d_solver.getSynthSolution(f), CVC5ApiException); - d_solver.checkSynth(); + cvc5::api::SynthResult sr = d_solver.checkSynth(); + ASSERT_EQ(sr.hasSolution(), true); ASSERT_NO_THROW(d_solver.getSynthSolution(f)); ASSERT_NO_THROW(d_solver.getSynthSolution(f)); @@ -2722,9 +2723,11 @@ TEST_F(TestApiBlackSolver, checkSynthNext) d_solver.setOption("incremental", "true"); Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort()); - d_solver.checkSynth(); + cvc5::api::SynthResult sr = d_solver.checkSynth(); + ASSERT_EQ(sr.hasSolution(), true); ASSERT_NO_THROW(d_solver.getSynthSolutions({f})); - d_solver.checkSynthNext(); + sr = d_solver.checkSynthNext(); + ASSERT_EQ(sr.hasSolution(), true); ASSERT_NO_THROW(d_solver.getSynthSolutions({f})); } diff --git a/test/unit/api/cpp/synth_result_black.cpp b/test/unit/api/cpp/synth_result_black.cpp index d2aebdbc4..813138323 100644 --- a/test/unit/api/cpp/synth_result_black.cpp +++ b/test/unit/api/cpp/synth_result_black.cpp @@ -34,5 +34,41 @@ TEST_F(TestApiBlackSynthResult, isNull) ASSERT_FALSE(res_null.isUnknown()); } +TEST_F(TestApiBlackSynthResult, hasSolution) +{ + d_solver.setOption("sygus", "true"); + Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort()); + Term boolTerm = d_solver.mkTrue(); + d_solver.addSygusConstraint(boolTerm); + cvc5::api::SynthResult res = d_solver.checkSynth(); + ASSERT_FALSE(res.isNull()); + ASSERT_TRUE(res.hasSolution()); + ASSERT_FALSE(res.hasNoSolution()); + ASSERT_FALSE(res.isUnknown()); +} + +TEST_F(TestApiBlackSynthResult, hasNoSolution) +{ + // note that we never return synth result for which hasNoSolution is true + // currently + cvc5::api::SynthResult res_null; + ASSERT_FALSE(res_null.hasNoSolution()); +} + +TEST_F(TestApiBlackSynthResult, isUnknown) +{ + d_solver.setOption("sygus", "true"); + Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort()); + Term boolTerm = d_solver.mkFalse(); + d_solver.addSygusConstraint(boolTerm); + cvc5::api::SynthResult res = d_solver.checkSynth(); + // currently isUnknown, could also return hasNoSolution when support for + // infeasibility of sygus conjectures is added. + ASSERT_FALSE(res.isNull()); + ASSERT_FALSE(res.hasSolution()); + ASSERT_FALSE(res.hasNoSolution()); + ASSERT_TRUE(res.isUnknown()); +} + } // namespace test } // namespace cvc5 diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index fe5afeee6..1c01e32b5 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -2641,7 +2641,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolution(f)); - d_solver.checkSynth(); + SynthResult sr = d_solver.checkSynth(); + assertEquals(sr.hasSolution(), true); assertDoesNotThrow(() -> d_solver.getSynthSolution(f)); assertDoesNotThrow(() -> d_solver.getSynthSolution(f)); @@ -2685,9 +2686,11 @@ class SolverTest d_solver.setOption("incremental", "true"); Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort()); - d_solver.checkSynth(); + SynthResult sr = d_solver.checkSynth(); + assertEquals(sr.hasSolution(), true); assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f})); - d_solver.checkSynthNext(); + sr = d_solver.checkSynthNext(); + assertEquals(sr.hasSolution(), true); assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f})); } diff --git a/test/unit/api/java/SynthResultTest.java b/test/unit/api/java/SynthResultTest.java index 058decd0b..efc82a816 100644 --- a/test/unit/api/java/SynthResultTest.java +++ b/test/unit/api/java/SynthResultTest.java @@ -44,4 +44,36 @@ class SynthResultTest assertFalse(res_null.hasNoSolution()); assertFalse(res_null.isUnknown()); } + + @Test void hasSolution() + { + d_solver.setOption("sygus", "true"); + Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort()); + Term boolTerm = d_solver.mkTrue(); + d_solver.addSygusConstraint(boolTerm); + SynthResult res = d_solver.checkSynth(); + assertFalse(res.isNull()); + assertTrue(res.hasSolution()); + assertFalse(res.hasNoSolution()); + assertFalse(res.isUnknown()); + } + + @Test void hasNoSolution() + { + SynthResult res_null = d_solver.getNullSynthResult(); + assertFalse(res_null.hasSolution()); + } + + @Test void isUnknown() + { + d_solver.setOption("sygus", "true"); + Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort()); + Term boolTerm = d_solver.mkTrue(); + d_solver.addSygusConstraint(boolTerm); + SynthResult res = d_solver.checkSynth(); + assertFalse(res.isNull()); + assertTrue(res.hasSolution()); + assertFalse(res.hasNoSolution()); + assertFalse(res.isUnknown()); + } } diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 6f18d96b4..099b1171b 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -2046,7 +2046,8 @@ def test_get_synth_solution(solver): with pytest.raises(RuntimeError): solver.getSynthSolution(f) - solver.checkSynth() + res = solver.checkSynth() + assert res.hasSolution() solver.getSynthSolution(f) solver.getSynthSolution(f) @@ -2065,10 +2066,12 @@ def test_check_synth_next(solver): solver.setOption("incremental", "true") f = solver.synthFun("f", [], solver.getBooleanSort()) - solver.checkSynth() + res = solver.checkSynth() + assert res.hasSolution() solver.getSynthSolutions([f]) - solver.checkSynthNext() + res = solver.checkSynthNext() + assert res.hasSolution() solver.getSynthSolutions([f]) def test_check_synth_next2(solver): diff --git a/test/unit/api/python/test_synth_result.py b/test/unit/api/python/test_synth_result.py index a07b635de..27ff9f2d2 100644 --- a/test/unit/api/python/test_synth_result.py +++ b/test/unit/api/python/test_synth_result.py @@ -31,3 +31,29 @@ def test_is_null(solver): assert not res_null.hasSolution() assert not res_null.hasNoSolution() assert not res_null.isUnknown() + +def test_has_solution(solver): + solver.setOption("sygus", "true") + f = solver.synthFun("f", [], solver.getBooleanSort()) + boolTerm = solver.mkBoolean(True) + solver.addSygusConstraint(boolTerm) + res = solver.checkSynth() + assert not res_null.isNull() + assert res_null.hasSolution() + assert not res_null.hasNoSolution() + assert not res_null.isUnknown() + +def test_has_no_solution(solver): + res_null = SynthResult(solver) + assert not res_null.hasNoSolution() + +def test_has_is_unknown(solver): + solver.setOption("sygus", "true") + f = solver.synthFun("f", [], solver.getBooleanSort()) + boolTerm = solver.mkBoolean(False) + solver.addSygusConstraint(boolTerm) + res = solver.checkSynth() + assert not res_null.isNull() + assert not res_null.hasSolution() + assert not res_null.hasNoSolution() + assert res_null.isUnknown() -- 2.30.2