git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 25 Mar 2022 20:00:14 +0000 (15:00 -0500)
committer	GitHub <noreply@github.com>
	Fri, 25 Mar 2022 20:00:14 +0000 (20:00 +0000)
commit	bf8ec7d9f13a9b37d9b5b279167b77cf28d74c45
tree	2335b66f7dfb05cae36b7f3a7f4c1dd567d41aec	tree
parent	219e2763d670e7bad8d6178fa4dd80b5bf1f6ea8	commit \| diff

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.

233 files changed:

examples/api/cpp/sygus-fun.cpp		diff \| blob \| history
examples/api/cpp/sygus-grammar.cpp		diff \| blob \| history
examples/api/cpp/sygus-inv.cpp		diff \| blob \| history
examples/api/java/SygusFun.java		diff \| blob \| history
examples/api/java/SygusGrammar.java		diff \| blob \| history
examples/api/java/SygusInv.java		diff \| blob \| history
examples/api/python/sygus-fun.py		diff \| blob \| history
examples/api/python/sygus-grammar.py		diff \| blob \| history
examples/api/python/sygus-inv.py		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/java/io/github/cvc5/api/Solver.java		diff \| blob \| history
src/api/java/jni/solver.cpp		diff \| blob \| history
src/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.h		diff \| blob \| history
src/smt/solver_engine_state.cpp		diff \| blob \| history
src/smt/solver_engine_state.h		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
src/smt/sygus_solver.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
test/regress/cli/regress0/sygus/General_plus10.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/aig-si.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/array-grammar-select.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/assume-simple.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/c100.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/ccp16.lus.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/cegqi-si-string-triv-2fun.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/cegqi-si-string-triv.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/check-generic-red.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/const-var-test.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/dt-no-syntax.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/dt-sel-parse1.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/hd-05-d1-prog-nogrammar.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/ho-occ-synth-fun.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/incremental-modify-ex.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/inv-different-var-order.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/issue3624.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/issue4383-cache-fv-id.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/issue4790-dtd.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/issue6298-par.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/let-ringer.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/let-simp.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/no-logic.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/no-syntax-test-bool.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/no-syntax-test.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/parity-AIG-d0.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/parse-bv-let.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/pbe-pred-contra.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/real-si-all.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/strings-unconstrained.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/sygus-no-wf.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/sygus-uf.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/uminus_one.sy		diff \| blob \| history
test/regress/cli/regress0/sygus/univ_3-long-repeat-conflict.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/Base16_1.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/VC22_a.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/abv.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/array-grammar-store.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/array-uc.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/array_search_2.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/array_search_5-Q-easy.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/array_sum_2_5.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/bvudiv-by-2.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/car_3.lus.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/cegar1.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/cegis-unif-inv-eq-fair.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/cggmp.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/clock-inc-tuple.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/coeff-solve-inv.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/commutative.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/complex-no-rewrite.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/complex-rewrite-in-db.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/concat_extract_example.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/constant-bool-si-all.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/constant-dec-tree-bug.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/constant-ite-bv.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/constant.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/crci-ssb-unk.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/crcy-si-rcons.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/crcy-si.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/cube-nia.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/discPresent.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/double.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/dt-test-ns.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/dup-op.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/eq-sub-obs.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/error1-dt.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/eval-uc.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/extract.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/fast-enum-backtrack.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/fg_polynomial3.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/find_sc_bvult_bvnot.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/ground-ite-free-constant-si.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/hd-01-d1-prog.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/hd-19-d1-prog-dup-op.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/hd-sdiv.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/ho-sygus.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/icfp_14.12-flip-args.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/icfp_14.12.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/icfp_14_12_diff_types.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/icfp_28_10.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/icfp_easy-ite.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/incremental-stream-ex.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/int-any-const.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/inv-example.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/inv-missed-sol-true.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/inv-unused.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/inv_gen_fig8.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/issue2914.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/issue2935.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3109-share-sel.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3320-quant.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3461.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3580.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3649.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3802-default-consts.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/large-const-simp.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/let-bug-simp.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/list-head-x.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/list_recursor.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/logiccell_help.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/max-all.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/max-limit.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/max-try1.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/max-try2.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/max.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/max2-bv.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/multi-fun-polynomial2.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/nflat-fwd-3.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/nflat-fwd.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/nia-max-square-ns.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/no-flat-simp.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/no-mention.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/node-discrete.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/once_2.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/only-const-grammar.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/pLTL_5_trace.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/parity-si-rcons.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/pbe_multi.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/phone-1-long.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/planning-unif.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/process-10-vars.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/qe.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rand_const.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rand_p_0.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rand_p_1.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/re-concat.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/real-any-const.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/real-grammar.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rec-fun-swap.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rec-fun-sygus.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rec-fun-while-1.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rec-fun-while-2.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rec-fun-while-infinite.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/repair-const-rl.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/replicate-mod-assume.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/replicate-mod.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/rex-strings-alarm.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/sets-pred-test.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/simple-no-rewrite.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/simple-not-in-grammar.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/simple-regexp.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/simple-rewrite-in-db.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/simple-rewrite-not-in-db.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/stopwatch-bt.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-any-term1.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-concat-3-args.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-double-rec.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-no-syntax.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-small.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-template-infer-unused.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-template-infer.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-trivial-simp.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-trivial-two-type.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/strings-trivial.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/sygus-dt.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/sygus-lambda-fv.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/sygus-uf-ex.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/t8.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/temp_input_to_synth_ic-error-121418.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/tester.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/tl-type-0.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/tl-type-4x.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/tl-type.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/triv-type-mismatch-si.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/twolets1.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/twolets2-orig.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/unbdd_inv_gen_winf1.sy		diff \| blob \| history
test/regress/cli/regress1/sygus/univ_2-long-repeat.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/MPwL_d1s3.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/array_sum_dd.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/cegisunif-depth1-bv.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/ex23.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/examples-deq.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/icfp_easy_mt_ite.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/lustre-real.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/max2-univ.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/min_IC_1.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/mpg_guard1-dd.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/multi-udiv.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/no-bad-filter.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/no-syntax-test-no-si.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/pbe_bvurem.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/process-10-vars-2fun.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/process-arg-invariance.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/proj-issue119.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/real-grammar-neg.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/sets-fun-test.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/strings-no-syntax-len.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/sumn_recur_synth.sy		diff \| blob \| history
test/regress/cli/regress2/sygus/three.sy		diff \| blob \| history
test/regress/cli/regress3/DRAGON_1.lus.sy		diff \| blob \| history
test/regress/cli/regress3/cegisunif-depth1.sy		diff \| blob \| history
test/regress/cli/regress3/inv_gen_n_c11.sy		diff \| blob \| history
test/regress/cli/regress3/nia-max-square.sy		diff \| blob \| history
test/regress/cli/regress3/policyM.sy		diff \| blob \| history
test/regress/cli/regress3/sixfuncs.sy		diff \| blob \| history
test/regress/cli/regress3/strings-any-term.sy		diff \| blob \| history
test/regress/cli/regress3/unbdd_inv_gen_ex7.sy		diff \| blob \| history
test/regress/cli/regress3/unifpi-solve-car_1.lus.sy		diff \| blob \| history
test/regress/cli/regress3/vcb.sy		diff \| blob \| history
test/unit/api/cpp/solver_black.cpp		diff \| blob \| history
test/unit/api/cpp/synth_result_black.cpp		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history
test/unit/api/java/SynthResultTest.java		diff \| blob \| history
test/unit/api/python/test_solver.py		diff \| blob \| history
test/unit/api/python/test_synth_result.py		diff \| blob \| history

RSS Atom