From ad7907adff119a6e25fe3c229663afecb15db7c4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 20 Apr 2020 19:47:35 -0500 Subject: [PATCH] Make option names related to CEGQI consistent (#4316) This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus. Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit. The changes were done by these commands in the given directories: src/: for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done test/regress/: for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done src/: and test/regress/: for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done test/regress/: for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done test/regress/: for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done And a few minor fixes afterwards. This should be merged close to the time of the next stable release. --- .../smt-comp/run-script-smtcomp-current | 20 +- .../run-script-smtcomp-current-unsat-cores | 4 +- src/options/didyoumean_test.cpp | 8 +- src/options/quantifiers_options.toml | 104 +++++----- src/preprocessing/passes/global_negate.cpp | 8 +- src/smt/set_defaults.cpp | 46 ++--- src/theory/datatypes/sygus_extension.cpp | 14 +- src/theory/quantifiers/bv_inverter.cpp | 2 +- .../cegqi/ceg_arith_instantiator.cpp | 34 ++-- .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 20 +- .../quantifiers/cegqi/ceg_instantiator.cpp | 190 +++++++++--------- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 96 ++++----- .../ematching/candidate_generator.cpp | 2 +- .../ematching/inst_match_generator.cpp | 2 +- src/theory/quantifiers/equality_query.cpp | 2 +- .../quantifiers/inst_strategy_enumerative.cpp | 2 +- src/theory/quantifiers/instantiate.cpp | 2 +- .../quantifiers/quant_conflict_find.cpp | 2 +- .../sygus/ce_guided_single_inv.cpp | 40 ++-- src/theory/quantifiers/sygus/cegis.cpp | 10 +- .../quantifiers/sygus/sygus_enumerator.cpp | 6 +- .../quantifiers/sygus/sygus_repair_const.cpp | 10 +- .../quantifiers/sygus/synth_conjecture.cpp | 54 ++--- src/theory/quantifiers/sygus/synth_engine.cpp | 38 ++-- src/theory/quantifiers_engine.cpp | 2 +- test/regress/regress0/expect/scrub.08.sy | 2 +- test/regress/regress0/quantifiers/ari056.smt2 | 2 +- .../quantifiers/cbqi-lia-dt-simp.smt2 | 2 +- .../regress0/quantifiers/issue4086-infs.smt2 | 4 +- .../quantifiers/issue4275-qcf-cegqi-rep.smt2 | 2 +- .../quantifiers/mix-complete-strat.smt2 | 2 +- .../regress0/quantifiers/pure_dt_cbqi.smt2 | 2 +- .../regress0/quantifiers/qbv-inequality2.smt2 | 2 +- .../quantifiers/qbv-multi-lit-uge.smt2 | 2 +- .../regress0/quantifiers/qbv-simp.smt2 | 2 +- .../qbv-test-invert-bvadd-neq.smt2 | 2 +- .../qbv-test-invert-bvand-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvand.smt2 | 2 +- .../qbv-test-invert-bvashr-0-neq.smt2 | 2 +- .../qbv-test-invert-bvashr-1-neq.smt2 | 2 +- .../qbv-test-invert-bvlshr-0-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvlshr-0.smt2 | 2 +- .../qbv-test-invert-bvlshr-1-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvor-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvor.smt2 | 2 +- .../qbv-test-invert-bvshl-0-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvshl-0.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvult-1.smt2 | 2 +- .../qbv-test-invert-bvxor-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvxor.smt2 | 2 +- .../qbv-test-invert-concat-0-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-concat-0.smt2 | 2 +- .../qbv-test-invert-concat-1-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-concat-1.smt2 | 2 +- .../qbv-test-invert-sign-extend.smt2 | 2 +- test/regress/regress0/sygus/General_plus10.sy | 2 +- test/regress/regress0/sygus/aig-si.sy | 2 +- test/regress/regress0/sygus/c100.sy | 2 +- .../regress0/sygus/check-generic-red.sy | 2 +- test/regress/regress0/sygus/const-var-test.sy | 2 +- .../regress0/sygus/hd-05-d1-prog-nogrammar.sy | 2 +- test/regress/regress0/sygus/let-ringer.sy | 4 +- test/regress/regress0/sygus/let-simp.sy | 2 +- test/regress/regress0/sygus/parity-AIG-d0.sy | 2 +- .../regress/regress0/sygus/pbe-pred-contra.sy | 2 +- test/regress/regress1/bug519.smt2 | 2 +- test/regress/regress1/quantifiers/NUM878.smt2 | 2 +- .../quantifiers/RNDPRE_4_1-dd-nqe.smt2 | 2 +- .../regress1/quantifiers/anti-sk-simp.smt2 | 2 +- .../quantifiers/ari118-bv-2occ-x.smt2 | 2 +- .../quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 | 2 +- .../regress1/quantifiers/extract-nproc.smt2 | 2 +- ...ction-example-onelane.proof-node22337.smt2 | 2 +- .../quantifiers/issue4243-prereg-inc.smt2 | 2 +- .../regress1/quantifiers/lra-vts-inf.smt2 | 2 +- .../regress1/quantifiers/model_6_1_bv.smt2 | 2 +- .../nested9_true-unreach-call.i_575.smt2 | 2 +- .../regress1/quantifiers/nl-pow-trick.smt2 | 2 +- .../quantifiers/nra-interleave-inst.smt2 | 2 +- .../regress1/quantifiers/psyco-107-bv.smt2 | 2 +- .../quantifiers/qbv-disequality3.smt2 | 2 +- .../quantifiers/qbv-simple-2vars-vo.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvashr-0.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvashr-1.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvcomp.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvlshr-1.smt2 | 2 +- .../qbv-test-invert-bvmul-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvmul.smt2 | 2 +- .../qbv-test-invert-bvudiv-0-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvudiv-0.smt2 | 2 +- .../qbv-test-invert-bvudiv-1-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvudiv-1.smt2 | 2 +- .../qbv-test-invert-bvurem-1-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvurem-1.smt2 | 2 +- .../quantifiers/qbv-test-urem-rewrite.smt2 | 2 +- .../small-pipeline-fixpoint-3.smt2 | 2 +- test/regress/regress1/sygus/Base16_1.sy | 2 +- test/regress/regress1/sygus/array_search_2.sy | 2 +- .../regress1/sygus/array_search_5-Q-easy.sy | 2 +- test/regress/regress1/sygus/array_sum_2_5.sy | 2 +- .../regress/regress1/sygus/clock-inc-tuple.sy | 2 +- test/regress/regress1/sygus/crcy-si-rcons.sy | 2 +- test/regress/regress1/sygus/dt-test-ns.sy | 2 +- test/regress/regress1/sygus/dup-op.sy | 2 +- test/regress/regress1/sygus/enum-test.sy | 2 +- test/regress/regress1/sygus/error1-dt.sy | 2 +- .../regress1/sygus/hd-19-d1-prog-dup-op.sy | 2 +- test/regress/regress1/sygus/hd-sdiv.sy | 2 +- test/regress/regress1/sygus/int-any-const.sy | 2 +- .../regress1/sygus/large-const-simp.sy | 2 +- test/regress/regress1/sygus/list-head-x.sy | 2 +- test/regress/regress1/sygus/max.sy | 2 +- .../regress1/sygus/nia-max-square-ns.sy | 2 +- .../regress/regress1/sygus/parity-si-rcons.sy | 2 +- test/regress/regress1/sygus/phone-1-long.sy | 2 +- .../regress/regress1/sygus/process-10-vars.sy | 2 +- test/regress/regress1/sygus/qe.sy | 2 +- test/regress/regress1/sygus/real-any-const.sy | 2 +- test/regress/regress1/sygus/real-grammar.sy | 2 +- .../regress/regress1/sygus/repair-const-rl.sy | 2 +- .../regress1/sygus/strings-any-term1.sy | 2 +- test/regress/regress1/sygus/tl-type-0.sy | 2 +- test/regress/regress1/sygus/tl-type-4x.sy | 2 +- test/regress/regress1/sygus/tl-type.sy | 2 +- test/regress/regress1/sygus/twolets1.sy | 2 +- test/regress/regress1/sygus/twolets2-orig.sy | 2 +- .../quantifiers/small-bug1-fixpoint-3.smt2 | 2 +- test/regress/regress2/sygus/lustre-real.sy | 2 +- .../regress2/sygus/process-10-vars-2fun.sy | 2 +- .../regress2/sygus/process-arg-invariance.sy | 2 +- .../regress2/sygus/real-grammar-neg.sy | 2 +- test/regress/regress3/strings-any-term.sy | 2 +- .../theory_quantifiers_bv_inverter_white.h | 2 +- 133 files changed, 469 insertions(+), 469 deletions(-) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index b46253851..b0bc70cd7 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -90,24 +90,24 @@ ABVFP|BVFP|FP) UFBV) # most problems in UFBV are essentially BV trywith 600 --full-saturate-quant --decision=internal - trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal - trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate + trywith 600 --full-saturate-quant --cegqi-nested-qe --decision=internal + trywith 60 --full-saturate-quant --no-cegqi-innermost --global-negate finishwith --finite-model-find ;; BV) trywith 240 --full-saturate-quant - trywith 240 --full-saturate-quant --no-cbqi-innermost - trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal - trywith 60 --full-saturate-quant --no-cbqi-bv - trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack + trywith 240 --full-saturate-quant --no-cegqi-innermost + trywith 600 --full-saturate-quant --cegqi-nested-qe --decision=internal + trywith 60 --full-saturate-quant --no-cegqi-bv + trywith 60 --full-saturate-quant --cegqi-bv-ineq=eq-slack # finish 10min - finishwith --full-saturate-quant --no-cbqi-innermost --global-negate + finishwith --full-saturate-quant --no-cegqi-innermost --global-negate ;; LIA|LRA|NIA|NRA) trywith 60 --full-saturate-quant --nl-ext-tplanes - trywith 600 --full-saturate-quant --no-cbqi-innermost - trywith 600 --full-saturate-quant --cbqi-nested-qe - finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + trywith 600 --full-saturate-quant --no-cegqi-innermost + trywith 600 --full-saturate-quant --cegqi-nested-qe + finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal ;; QF_AUFBV) trywith 1200 --ite-simp diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores index 0371d8b42..5e827128e 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -36,10 +36,10 @@ BV) finishwith --full-saturate-quant --decision=internal ;; LIA|LRA) - finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal ;; NIA|NRA) - finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal ;; QF_AUFBV) finishwith --decision=justification-stoponly --ite-simp diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp index df1dfa5cc..2dd28a40f 100644 --- a/src/options/didyoumean_test.cpp +++ b/src/options/didyoumean_test.cpp @@ -165,9 +165,9 @@ set getDebugTags() { a.insert("bvminisat"); a.insert("bvminisat::explain"); a.insert("bvminisat::search"); - a.insert("cbqi"); - a.insert("cbqi-debug"); - a.insert("cbqi-prop-as-dec"); + a.insert("cegqi"); + a.insert("cegqi-debug"); + a.insert("cegqi-prop-as-dec"); a.insert("cd_set_collection"); a.insert("cdlist"); a.insert("cdlist:cmm"); @@ -605,7 +605,7 @@ set getOptionStrings() { "literal-matching", "enable-cbqi", "no-enable-cbqi", - "cbqi-recurse", + "cegqi-recurse", "no-cbqi-recurse", "user-pat", "flip-decision", diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 32ae173bd..21cba6abb 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -987,7 +987,7 @@ header = "options/quantifiers_options.h" [[option]] name = "cegqiSingleInvMode" category = "regular" - long = "cegqi-si=MODE" + long = "sygus-si=MODE" type = "CegqiSingleInvMode" default = "NONE" help = "mode for processing single invocation synthesis conjectures" @@ -1005,7 +1005,7 @@ header = "options/quantifiers_options.h" [[option]] name = "cegqiSingleInvPartial" category = "regular" - long = "cegqi-si-partial" + long = "sygus-si-partial" type = "bool" default = "false" read_only = true @@ -1020,7 +1020,7 @@ header = "options/quantifiers_options.h" [[option]] name = "cegqiSingleInvReconstruct" category = "regular" - long = "cegqi-si-rcons=MODE" + long = "sygus-si-rcons=MODE" type = "CegqiSingleInvRconsMode" default = "ALL_LIMIT" help = "policy for reconstructing solutions for single invocation conjectures" @@ -1041,7 +1041,7 @@ header = "options/quantifiers_options.h" [[option]] name = "cegqiSingleInvReconstructLimit" category = "regular" - long = "cegqi-si-rcons-limit=N" + long = "sygus-si-rcons-limit=N" type = "int" default = "10000" read_only = true @@ -1050,7 +1050,7 @@ header = "options/quantifiers_options.h" [[option]] name = "cegqiSingleInvReconstructConst" category = "regular" - long = "cegqi-si-reconstruct-const" + long = "sygus-si-reconstruct-const" type = "bool" default = "true" read_only = true @@ -1059,7 +1059,7 @@ header = "options/quantifiers_options.h" [[option]] name = "cegqiSingleInvAbort" category = "regular" - long = "cegqi-si-abort" + long = "sygus-si-abort" type = "bool" default = "false" read_only = true @@ -1623,73 +1623,73 @@ header = "options/quantifiers_options.h" # CEGQI applied to general quantified formulas [[option]] - name = "cbqi" + name = "cegqi" category = "regular" - long = "cbqi" + long = "cegqi" type = "bool" default = "false" help = "turns on counterexample-based quantifier instantiation" [[option]] - name = "cbqiFullEffort" + name = "cegqiFullEffort" category = "regular" - long = "cbqi-full" + long = "cegqi-full" type = "bool" default = "false" help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation" [[option]] - name = "cbqiSat" + name = "cegqiSat" category = "regular" - long = "cbqi-sat" + long = "cegqi-sat" type = "bool" default = "true" help = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation" [[option]] - name = "cbqiModel" + name = "cegqiModel" category = "regular" - long = "cbqi-model" + long = "cegqi-model" type = "bool" default = "true" help = "guide instantiations by model values for counterexample-based quantifier instantiation" [[option]] - name = "cbqiAll" + name = "cegqiAll" category = "regular" - long = "cbqi-all" + long = "cegqi-all" type = "bool" default = "false" help = "apply counterexample-based instantiation to all quantified formulas" [[option]] - name = "cbqiMultiInst" + name = "cegqiMultiInst" category = "regular" - long = "cbqi-multi-inst" + long = "cegqi-multi-inst" type = "bool" default = "false" help = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation" [[option]] - name = "cbqiRepeatLit" + name = "cegqiRepeatLit" category = "regular" - long = "cbqi-repeat-lit" + long = "cegqi-repeat-lit" type = "bool" default = "false" help = "solve literals more than once in counterexample-based quantifier instantiation" [[option]] - name = "cbqiInnermost" + name = "cegqiInnermost" category = "regular" - long = "cbqi-innermost" + long = "cegqi-innermost" type = "bool" default = "true" help = "only process innermost quantified formulas in counterexample-based quantifier instantiation" [[option]] - name = "cbqiNestedQE" + name = "cegqiNestedQE" category = "regular" - long = "cbqi-nested-qe" + long = "cegqi-nested-qe" type = "bool" default = "false" help = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation" @@ -1697,59 +1697,59 @@ header = "options/quantifiers_options.h" # CEGQI for arithmetic [[option]] - name = "cbqiUseInfInt" + name = "cegqiUseInfInt" category = "regular" - long = "cbqi-use-inf-int" + long = "cegqi-use-inf-int" type = "bool" default = "false" help = "use integer infinity for vts in counterexample-based quantifier instantiation" [[option]] - name = "cbqiUseInfReal" + name = "cegqiUseInfReal" category = "regular" - long = "cbqi-use-inf-real" + long = "cegqi-use-inf-real" type = "bool" default = "false" help = "use real infinity for vts in counterexample-based quantifier instantiation" [[option]] - name = "cbqiPreRegInst" + name = "cegqiPreRegInst" category = "regular" - long = "cbqi-prereg-inst" + long = "cegqi-prereg-inst" type = "bool" default = "false" help = "preregister ground instantiations in counterexample-based quantifier instantiation" [[option]] - name = "cbqiMinBounds" + name = "cegqiMinBounds" category = "regular" - long = "cbqi-min-bounds" + long = "cegqi-min-bounds" type = "bool" default = "false" read_only = true help = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation" [[option]] - name = "cbqiRoundUpLowerLia" + name = "cegqiRoundUpLowerLia" category = "regular" - long = "cbqi-round-up-lia" + long = "cegqi-round-up-lia" type = "bool" default = "false" read_only = true help = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation" [[option]] - name = "cbqiMidpoint" + name = "cegqiMidpoint" category = "regular" - long = "cbqi-midpoint" + long = "cegqi-midpoint" type = "bool" default = "false" help = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation" [[option]] - name = "cbqiNopt" + name = "cegqiNopt" category = "regular" - long = "cbqi-nopt" + long = "cegqi-nopt" type = "bool" default = "true" read_only = true @@ -1777,25 +1777,25 @@ header = "options/quantifiers_options.h" # CEGQI for BV [[option]] - name = "cbqiBv" + name = "cegqiBv" category = "regular" - long = "cbqi-bv" + long = "cegqi-bv" type = "bool" default = "true" help = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors" [[option]] - name = "cbqiBvInterleaveValue" + name = "cegqiBvInterleaveValue" category = "regular" - long = "cbqi-bv-interleave-value" + long = "cegqi-bv-interleave-value" type = "bool" default = "false" help = "interleave model value instantiation with word-level inversion approach" [[option]] - name = "cbqiBvIneqMode" + name = "cegqiBvIneqMode" category = "regular" - long = "cbqi-bv-ineq=MODE" + long = "cegqi-bv-ineq=MODE" type = "CbqiBvIneqMode" default = "EQ_BOUNDARY" help = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation" @@ -1811,33 +1811,33 @@ header = "options/quantifiers_options.h" help = "Solve for the inequality directly using side conditions for invertibility." [[option]] - name = "cbqiBvRmExtract" + name = "cegqiBvRmExtract" category = "regular" - long = "cbqi-bv-rm-extract" + long = "cegqi-bv-rm-extract" type = "bool" default = "true" help = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors" [[option]] - name = "cbqiBvLinearize" + name = "cegqiBvLinearize" category = "regular" - long = "cbqi-bv-linear" + long = "cegqi-bv-linear" type = "bool" default = "true" help = "linearize adder chains for variables" [[option]] - name = "cbqiBvSolveNl" + name = "cegqiBvSolveNl" category = "regular" - long = "cbqi-bv-solve-nl" + long = "cegqi-bv-solve-nl" type = "bool" default = "false" help = "try to solve non-linear bv literals using model value projections" [[option]] - name = "cbqiBvConcInv" + name = "cegqiBvConcInv" category = "regular" - long = "cbqi-bv-concat-inv" + long = "cegqi-bv-concat-inv" type = "bool" default = "true" help = "compute inverse for concat over equalities rather than producing an invertibility condition" diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 5e7d42632..59b5ddf6e 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -30,14 +30,14 @@ namespace passes { Node GlobalNegate::simplify(std::vector& assertions, NodeManager* nm) { Assert(!assertions.empty()); - Trace("cbqi-gn") << "Global negate : " << std::endl; + Trace("cegqi-gn") << "Global negate : " << std::endl; // collect free variables in all assertions std::vector free_vars; std::vector visit; std::unordered_set visited; for (const Node& as : assertions) { - Trace("cbqi-gn") << " " << as << std::endl; + Trace("cegqi-gn") << " " << as << std::endl; TNode cur = as; // compute free variables visit.push_back(cur); @@ -90,9 +90,9 @@ Node GlobalNegate::simplify(std::vector& assertions, NodeManager* nm) body = nm->mkNode(FORALL, bvl, body); } - Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; + Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; body = Rewriter::rewrite(body); - Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl; + Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl; return body; } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 7109a3222..f98c9ee84 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -495,7 +495,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } } - if (options::cbqiBv() && logic.isQuantified()) + if (options::cegqiBv() && logic.isQuantified()) { if (options::boolToBitvector() != options::BoolToBVMode::OFF) { @@ -819,11 +819,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << std::endl; - options::cbqi.set(false); + options::cegqi.set(false); } // Do we need to track instantiations? // Needed for sygus due to single invocation techniques. - if (options::cbqiNestedQE() + if (options::cegqiNestedQE() || (options::proof() && !options::trackInstLemmas.wasSetByUser()) || is_sygus) { @@ -937,15 +937,15 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } options::sygus.set(true); // must use Ferrante/Rackoff for real arithmetic - if (!options::cbqiMidpoint.wasSetByUser()) + if (!options::cegqiMidpoint.wasSetByUser()) { - options::cbqiMidpoint.set(true); + options::cegqiMidpoint.set(true); } if (options::sygusRepairConst()) { - if (!options::cbqi.wasSetByUser()) + if (!options::cegqi.wasSetByUser()) { - options::cbqi.set(true); + options::cegqi.set(true); } } if (options::sygusInference()) @@ -973,10 +973,10 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { options::instNoEntail.set(false); } - if (!options::cbqiFullEffort.wasSetByUser()) + if (!options::cegqiFullEffort.wasSetByUser()) { // should use full effort cbqi for single invocation and repair const - options::cbqiFullEffort.set(true); + options::cegqiFullEffort.set(true); } if (options::sygusRew()) { @@ -1085,9 +1085,9 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { options::macrosQuant.set(false); } - if (!options::cbqiPreRegInst.wasSetByUser()) + if (!options::cegqiPreRegInst.wasSetByUser()) { - options::cbqiPreRegInst.set(true); + options::cegqiPreRegInst.set(true); } } // counterexample-guided instantiation for non-sygus @@ -1097,22 +1097,22 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) || logic.isTheoryEnabled(THEORY_DATATYPES) || logic.isTheoryEnabled(THEORY_BV) || logic.isTheoryEnabled(THEORY_FP))) - || options::cbqiAll()) + || options::cegqiAll()) { - if (!options::cbqi.wasSetByUser()) + if (!options::cegqi.wasSetByUser()) { - options::cbqi.set(true); + options::cegqi.set(true); } // check whether we should apply full cbqi if (logic.isPure(THEORY_BV)) { - if (!options::cbqiFullEffort.wasSetByUser()) + if (!options::cegqiFullEffort.wasSetByUser()) { - options::cbqiFullEffort.set(true); + options::cegqiFullEffort.set(true); } } } - if (options::cbqi()) + if (options::cegqi()) { // must rewrite divk if (!options::rewriteDivk.wasSetByUser()) @@ -1122,8 +1122,8 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) if (options::incrementalSolving()) { // cannot do nested quantifier elimination in incremental mode - options::cbqiNestedQE.set(false); - options::cbqiPreRegInst.set(false); + options::cegqiNestedQE.set(false); + options::cegqiPreRegInst.set(false); } if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV)) { @@ -1135,7 +1135,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { options::instNoEntail.set(false); } - if (!options::instWhenMode.wasSetByUser() && options::cbqiModel()) + if (!options::instWhenMode.wasSetByUser() && options::cegqiModel()) { // only instantiation should happen at last call when model is avaiable options::instWhenMode.set(options::InstWhenMode::LAST_CALL); @@ -1144,10 +1144,10 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) else { // only supported in pure arithmetic or pure BV - options::cbqiNestedQE.set(false); + options::cegqiNestedQE.set(false); } // prenexing - if (options::cbqiNestedQE()) + if (options::cegqiNestedQE()) { // only complete with prenex = disj_normal or normal if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL) @@ -1175,7 +1175,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { options::quantConflictFind.set(true); } - if (options::cbqiNestedQE()) + if (options::cegqiNestedQE()) { options::prenexQuantUser.set(true); if (!options::preSkolemQuant.wasSetByUser()) diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index dbc1e24af..f22e0e6d5 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1623,26 +1623,26 @@ void SygusExtension::check( std::vector< Node >& lemmas ) { return check(lemmas); } - if (Trace.isOn("cegqi-engine") && !d_szinfo.empty()) + if (Trace.isOn("sygus-engine") && !d_szinfo.empty()) { if (lemmas.empty()) { - Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : "; + Trace("sygus-engine") << "*** Sygus : passed datatypes check. term size(s) : "; for (std::pair>& p : d_szinfo) { SygusSizeDecisionStrategy* s = p.second.get(); - Trace("cegqi-engine") << s->d_curr_search_size << " "; + Trace("sygus-engine") << s->d_curr_search_size << " "; } - Trace("cegqi-engine") << std::endl; + Trace("sygus-engine") << std::endl; } else { - Trace("cegqi-engine") + Trace("sygus-engine") << "*** Sygus : produced symmetry breaking lemmas" << std::endl; for (const Node& lem : lemmas) { - Trace("cegqi-engine-debug") << " " << lem << std::endl; + Trace("sygus-engine-debug") << " " << lem << std::endl; } } } @@ -1783,7 +1783,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s) } Assert(!d_this.isNull()); NodeManager* nm = NodeManager::currentNM(); - Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s + Trace("sygus-engine") << "******* Sygus : allocate size literal " << s << " for " << d_this << std::endl; return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s))); } diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index c349e05b0..3756c6b4b 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -336,7 +336,7 @@ Node BvInverter::solveBvLit(Node sv, } else if (k == BITVECTOR_CONCAT) { - if (litk == EQUAL && options::cbqiBvConcInv()) + if (litk == EQUAL && options::cegqiBvConcInv()) { /* Compute inverse for s1 o x, x o s2, s1 o x o s2 * (while disregarding that invertibility depends on si) diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 2984c23be..bb59aa766 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -167,7 +167,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, } // compute how many bounds we will consider unsigned rmax = 1; - if (atom.getKind() == EQUAL && (pol || !options::cbqiModel())) + if (atom.getKind() == EQUAL && (pol || !options::cegqiModel())) { rmax = 2; } @@ -206,7 +206,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, { // disequalities are either strict upper or lower bounds bool is_upper; - if (options::cbqiModel()) + if (options::cegqiModel()) { // disequality is a disjunction : only consider the bound in the // direction of the model @@ -273,7 +273,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, // take into account delta if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT) { - if (options::cbqiModel()) + if (options::cegqiModel()) { Node delta_coeff = nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)); @@ -295,7 +295,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, uval = Rewriter::rewrite(uval); } } - if (options::cbqiModel()) + if (options::cegqiModel()) { // just store bounds, will choose based on tighest bound unsigned index = isUpperBoundCTT(uires) ? 0 : 1; @@ -330,15 +330,15 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, Node pv, CegInstEffort effort) { - if (!options::cbqiModel()) + if (!options::cegqiModel()) { return false; } NodeManager* nm = NodeManager::currentNM(); bool use_inf = - d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal(); + d_type.isInteger() ? options::cegqiUseInfInt() : options::cegqiUseInfReal(); bool upper_first = Random::getRandom().pickWithProb(0.5); - if (options::cbqiMinBounds()) + if (options::cegqiMinBounds()) { upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size(); } @@ -370,7 +370,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cbqiMultiInst()) + else if (!options::cegqiMultiInst()) { return false; } @@ -509,7 +509,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, best_used[rr] = best; // if using cbqiMidpoint, only add the instance based on one bound if // the bound is non-strict - if (!options::cbqiMidpoint() || d_type.isInteger() + if (!options::cegqiMidpoint() || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull()) { Node val = d_mbp_bounds[rr][best]; @@ -532,7 +532,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cbqiMultiInst()) + else if (!options::cegqiMultiInst()) { return false; } @@ -563,13 +563,13 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cbqiMultiInst()) + else if (!options::cegqiMultiInst()) { return false; } } } - if (options::cbqiMidpoint() && !d_type.isInteger()) + if (options::cegqiMidpoint() && !d_type.isInteger()) { Node vals[2]; bool bothBounds = true; @@ -634,7 +634,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cbqiMultiInst()) + else if (!options::cegqiMultiInst()) { return false; } @@ -643,7 +643,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, // generally should not make it to this point, unless we are using a // non-monotonic selection function - if (!options::cbqiNopt()) + if (!options::cegqiNopt()) { // if not trying non-optimal bounds, return return false; @@ -656,7 +656,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++) { if ((int)j != best_used[rr] - && (!options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull())) + && (!options::cegqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull())) { Node val = getModelBasedProjectionValue(ci, pv, @@ -677,7 +677,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cbqiMultiInst()) + else if (!options::cegqiMultiInst()) { return false; } @@ -753,7 +753,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable( << "...bound type is : " << sf.d_props[index].d_type << std::endl; // intger division rounding up if from a lower bound if (sf.d_props[index].d_type == CEG_TT_UPPER - && options::cbqiRoundUpLowerLia()) + && options::cegqiRoundUpLowerLia()) { sf.d_subs[index] = nm->mkNode( PLUS, diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 92f3e6d0d..2d43e63dc 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -91,7 +91,7 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, Node pvs = ci->getModelValue(pv); Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl; Node slit = - d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl()); + d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cegqiBvSolveNl()); if (!slit.isNull()) { CegInstantiatorBvInverterQuery m(ci); @@ -153,7 +153,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, { return Node::null(); } - else if (options::cbqiBvIneqMode() == options::CbqiBvIneqMode::KEEP + else if (options::cegqiBvIneqMode() == options::CbqiBvIneqMode::KEEP || (pol && k == EQUAL)) { return lit; @@ -172,7 +172,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, Trace("cegqi-bv") << " " << sm << " <> " << tm << std::endl; Node ret; - if (options::cbqiBvIneqMode() == options::CbqiBvIneqMode::EQ_SLACK) + if (options::cegqiBvIneqMode() == options::CbqiBvIneqMode::EQ_SLACK) { // if using slack, we convert constraints to a positive equality based on // the current model M, e.g.: @@ -233,7 +233,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, { // if option enabled, use approach for word-level inversion for BV // instantiation - if (options::cbqiBv()) + if (options::cegqiBv()) { // get the best rewritten form of lit for solving for pv // this should remove instances of non-invertible operators, and @@ -261,7 +261,7 @@ bool BvInstantiator::useModelValue(CegInstantiator* ci, Node pv, CegInstEffort effort) { - return effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort(); + return effort < CEG_INST_EFFORT_FULL || options::cegqiFullEffort(); } bool BvInstantiator::processAssertions(CegInstantiator* ci, @@ -279,7 +279,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl; // if interleaving, do not do inversion half the time - if (options::cbqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5)) + if (options::cegqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5)) { Trace("cegqi-bv") << "...do not do instantiation for " << pv << " (skip, based on heuristic)" << std::endl; @@ -341,7 +341,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, // for constructing instantiations is exponential on the number of // variables in this quantifier prefix. bool ret = false; - bool tryMultipleInst = firstVar && options::cbqiMultiInst(); + bool tryMultipleInst = firstVar && options::cegqiMultiInst(); bool revertOnSuccess = tryMultipleInst; for (unsigned j = 0, size = iti->second.size(); j < size; j++) { @@ -557,7 +557,7 @@ Node BvInstantiator::rewriteTermForSolvePv( bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2)))); } - if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs]) + if (options::cegqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs]) { Node result = utils::normalizePvEqual(pv, children, contains_pv); if (!result.isNull()) @@ -575,7 +575,7 @@ Node BvInstantiator::rewriteTermForSolvePv( } else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS) { - if (options::cbqiBvLinearize() && contains_pv[n]) + if (options::cegqiBvLinearize() && contains_pv[n]) { Node result; if (n.getKind() == BITVECTOR_MULT) @@ -640,7 +640,7 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( // new lemmas std::vector new_lems; - if (options::cbqiBvRmExtract()) + if (options::cegqiBvRmExtract()) { NodeManager* nm = NodeManager::currentNM(); Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index e62de0840..6b625fc73 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -294,7 +294,7 @@ CegHandledStatus CegInstantiator::isCbqiTerm(Node n) if (curr < ret) { ret = curr; - Trace("cbqi-debug2") << "Non-cbqi kind : " << cur.getKind() + Trace("cegqi-debug2") << "Non-cbqi kind : " << cur.getKind() << " in " << n << std::endl; if (curr == CEG_UNHANDLED) { @@ -426,7 +426,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe) // if quantifier has a non-handled variable, then do not use cbqi // if quantifier has an APPLY_UF term, then do not use cbqi unless EPR CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q, qe); - Trace("cbqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv + Trace("cegqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv << std::endl; if (ncbqiv == CEG_UNHANDLED) { @@ -436,7 +436,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe) else { CegHandledStatus cbqit = CegInstantiator::isCbqiTerm(q); - Trace("cbqi-quant-debug") << "isCbqiTerm returned " << cbqit << std::endl; + Trace("cegqi-quant-debug") << "isCbqiTerm returned " << cbqit << std::endl; if (cbqit == CEG_UNHANDLED) { if (ncbqiv == CEG_HANDLED_UNCONDITIONAL) @@ -457,7 +457,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe) ret = CEG_PARTIALLY_HANDLED; } } - if (ret == CEG_UNHANDLED && options::cbqiAll()) + if (ret == CEG_UNHANDLED && options::cegqiAll()) { // try but not exclusively ret = CEG_PARTIALLY_HANDLED; @@ -549,7 +549,7 @@ void CegInstantiator::registerVariable(Node v) d_vars.push_back(v); d_vars_set.insert(v); TypeNode vtn = v.getType(); - Trace("cbqi-proc-debug") << "Collect theory ids from type " << vtn << " of " + Trace("cegqi-proc-debug") << "Collect theory ids from type " << vtn << " of " << v << std::endl; // collect relevant theories for this variable std::map visited; @@ -623,11 +623,11 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) } // If the above call fails, resort to using value in model. We do so if: // - we have yet to try an instantiation this round (or we are trying - // multiple instantiations, indicated by options::cbqiMultiInst), + // multiple instantiations, indicated by options::cegqiMultiInst), // - the instantiator uses model values at this effort or // if we are solving for a subfield of a datatype (is_sv), and // - the instantiator allows model values. - if ((options::cbqiMultiInst() || !hasTriedInstantiation(pv)) + if ((options::cegqiMultiInst() || !hasTriedInstantiation(pv)) && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv) && vinst->allowModelValue(this, sf, pv, d_effort)) { @@ -638,16 +638,16 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) // Quantified Linear Arithmetic by Counterexample Guided Instantiation", // FMSD 2017. We throw an assertion failure if we detect a case where the // strategy was not monotonic. - if (options::cbqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH) + if (options::cegqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH) && d_qe->getLogicInfo().isLinear()) { - Trace("cbqi-warn") << "Had to resort to model value." << std::endl; + Trace("cegqi-warn") << "Had to resort to model value." << std::endl; Assert(false); } #endif Node mv = getModelValue( pv ); TermProperties pv_prop_m; - Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; + Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE; CegInstEffort prev = d_effort; if (d_effort < CEG_INST_EFFORT_STANDARD_MV) @@ -662,7 +662,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) d_effort = prev; } - Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; + Trace("cegqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; if (is_sv) { d_stack_vars.push_back( pv ); @@ -684,34 +684,34 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { pvr = d_qe->getMasterEqualityEngine()->getRepresentative(pv); } - Trace("cbqi-inst-debug") << "[Find instantiation for " << pv + Trace("cegqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << ", instantiator is " << vinst->identify() << std::endl; Node pv_value; - if (options::cbqiModel()) + if (options::cegqiModel()) { pv_value = getModelValue(pv); - Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; + Trace("cegqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; } //[1] easy case : pv is in the equivalence class as another term not // containing pv if (vinst->hasProcessEqualTerm(this, sf, pv, d_effort)) { - Trace("cbqi-inst-debug") + Trace("cegqi-inst-debug") << "[1] try based on equivalence class." << std::endl; d_curr_iphase[pv] = CEG_INST_PHASE_EQC; std::map >::iterator it_eqc = d_curr_eqc.find(pvr); if (it_eqc != d_curr_eqc.end()) { // std::vector< Node > eq_candidates; - Trace("cbqi-inst-debug2") + Trace("cegqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl; for (const Node& n : it_eqc->second) { if (n != pv) { - Trace("cbqi-inst-debug") + Trace("cegqi-inst-debug") << "...try based on equal term " << n << std::endl; // must be an eligible term if (isEligible(n)) @@ -741,7 +741,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { return true; } - else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv)) + else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv)) { return false; } @@ -757,14 +757,14 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { return true; } - else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv)) + else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv)) { return false; } } else { - Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl; + Trace("cegqi-inst-debug2") << "...eqc not found." << std::endl; } } @@ -773,7 +773,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, /// the variable if (vinst->hasProcessEquality(this, sf, pv, d_effort)) { - Trace("cbqi-inst-debug") + Trace("cegqi-inst-debug") << "[2] try based on solving equalities." << std::endl; d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL; std::vector& cteqc = d_curr_type_eqc[pvtnb]; @@ -787,7 +787,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, Assert(it_reqc != d_curr_eqc.end()); for (const Node& n : it_reqc->second) { - Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; + Trace("cegqi-inst-debug2") << "...look at term " << n << std::endl; // must be an eligible term if (isEligible(n)) { @@ -808,7 +808,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, if (!ns.isNull()) { bool hasVar = d_prog_var[ns].find(pv) != d_prog_var[ns].end(); - Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv + Trace("cegqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; std::vector term_props; std::vector terms; @@ -819,7 +819,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, // if this term or the another has pv in it, try to solve for it if (hasVar || lhs_v[j]) { - Trace("cbqi-inst-debug") << "......try based on equality " + Trace("cegqi-inst-debug") << "......try based on equality " << lhs[j] << " = " << ns << std::endl; term_props.push_back(lhs_prop[j]); terms.push_back(lhs[j]); @@ -828,7 +828,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { return true; } - else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv)) + else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv)) { return false; } @@ -842,14 +842,14 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, } else { - Trace("cbqi-inst-debug2") + Trace("cegqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl; } } else { - Trace("cbqi-inst-debug2") + Trace("cegqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl; } } @@ -860,13 +860,13 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { return false; } - Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl; + Trace("cegqi-inst-debug") << "[3] try based on assertions." << std::endl; d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION; std::unordered_set lits; for (unsigned r = 0; r < 2; r++) { TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF; - Trace("cbqi-inst-debug2") << " look at assertions of " << tid << std::endl; + Trace("cegqi-inst-debug2") << " look at assertions of " << tid << std::endl; std::map >::iterator ita = d_curr_asserts.find(tid); if (ita != d_curr_asserts.end()) @@ -877,18 +877,18 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { lits.insert(lit); Node plit; - if (options::cbqiRepeatLit() || !isSolvedAssertion(lit)) + if (options::cegqiRepeatLit() || !isSolvedAssertion(lit)) { plit = vinst->hasProcessAssertion(this, sf, pv, lit, d_effort); } if (!plit.isNull()) { - Trace("cbqi-inst-debug2") << " look at " << lit; + Trace("cegqi-inst-debug2") << " look at " << lit; if (plit != lit) { - Trace("cbqi-inst-debug2") << "...processed to : " << plit; + Trace("cegqi-inst-debug2") << "...processed to : " << plit; } - Trace("cbqi-inst-debug2") << std::endl; + Trace("cegqi-inst-debug2") << std::endl; // apply substitutions Node slit = applySubstitutionToLiteral(plit, sf); if (!slit.isNull()) @@ -896,14 +896,14 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, // check if contains pv if (hasVariable(slit, pv)) { - Trace("cbqi-inst-debug") + Trace("cegqi-inst-debug") << "...try based on literal " << slit << "," << std::endl; - Trace("cbqi-inst-debug") << "...from " << lit << std::endl; + Trace("cegqi-inst-debug") << "...from " << lit << std::endl; if (vinst->processAssertion(this, sf, pv, slit, lit, d_effort)) { return true; } - else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv)) + else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv)) { return false; } @@ -939,14 +939,14 @@ bool CegInstantiator::constructInstantiationInc(Node pv, Node cnode = pv_prop.getCacheNode(); if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){ d_curr_subs_proc[pv][n][cnode] = true; - if( Trace.isOn("cbqi-inst-debug") ){ + if( Trace.isOn("cegqi-inst-debug") ){ for( unsigned j=0; j " << n << std::endl; + Trace("cegqi-inst-debug") << mod_pv << " -> " << n << std::endl; Assert(n.getType().isSubtypeOf(pv.getType())); } //must ensure variables have been computed for n @@ -969,9 +969,9 @@ bool CegInstantiator::constructInstantiationInc(Node pv, std::map< int, TermProperties > prev_prop; std::map< int, Node > prev_sym_subs; std::vector< Node > new_non_basic; - Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl; + Trace("cegqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl; for( unsigned j=0; j::iterator it = prev_subs.begin(); it != prev_subs.end(); @@ -1068,7 +1068,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv, bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) { if (vars.size() > d_input_vars.size() || !d_var_order_index.empty()) { - Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; + Trace("cegqi-inst-debug") << "Reconstructing instantiations...." << std::endl; std::map< Node, Node > subs_map; for( unsigned i=0; i& vars, std::vector std::map::iterator it = subs_map.find(d_input_vars[i]); Assert(it != subs_map.end()); Node n = it->second; - Trace("cbqi-inst-debug") << " " << d_input_vars[i] << " -> " << n + Trace("cegqi-inst-debug") << " " << d_input_vars[i] << " -> " << n << std::endl; Assert(n.getType().isSubtypeOf(d_input_vars[i].getType())); subs.push_back( n ); } } - if (Trace.isOn("cbqi-inst")) + if (Trace.isOn("cegqi-inst")) { - Trace("cbqi-inst") << "Ceg Instantiator produced : " << std::endl; + Trace("cegqi-inst") << "Ceg Instantiator produced : " << std::endl; for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i) { Node v = d_input_vars[i]; - Trace("cbqi-inst") << i << " (" << d_curr_iphase[v] << ") : " + Trace("cegqi-inst") << i << " (" << d_curr_iphase[v] << ") : " << v << " -> " << subs[i] << std::endl; Assert(subs[i].getType().isSubtypeOf(v.getType())); } } - Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl; + Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl; bool ret = d_parent->doAddInstantiation(subs); for( unsigned i=0; iaddLemma(lemmas[i]); @@ -1154,10 +1154,10 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node n = Rewriter::rewrite(n); computeProgVars( n ); bool is_basic = canApplyBasicSubstitution( n, non_basic ); - if( Trace.isOn("cegqi-si-apply-subs-debug") ){ - Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl; + if( Trace.isOn("sygus-si-apply-subs-debug") ){ + Trace("sygus-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl; for( unsigned i=0; i " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl; + Trace("sygus-si-apply-subs-debug") << " " << vars[i] << " -> " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl; Assert(subs[i].getType().isSubtypeOf(vars[i].getType())); } } @@ -1215,7 +1215,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node //make sum with normalized coefficient if( !pv_prop.d_coeff.isNull() ){ pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff ); - Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl; + Trace("sygus-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl; std::vector< Node > children; for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ Node c_coeff; @@ -1235,7 +1235,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); } children.push_back( c ); - Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl; + Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl; } Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); nretc = Rewriter::rewrite( nretc ); @@ -1245,14 +1245,14 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node //result is ( nret / pv_prop.d_coeff ) nret = nretc; }else{ - Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl; + Trace("sygus-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl; } }else{ //implies that we have a monomial that has a free variable - Trace("cegqi-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl; + Trace("sygus-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl; } }else{ - Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; + Trace("sygus-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; } } } @@ -1324,7 +1324,7 @@ bool CegInstantiator::check() { return true; } } - Trace("cbqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; return false; } @@ -1344,7 +1344,7 @@ void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq == it->second.end()) { it->second.push_back(nn); - Trace("cbqi-presolve") << " - " << n[i] << " = " << nn << std::endl; + Trace("cegqi-presolve") << " - " << n[i] << " = " << nn << std::endl; } } } @@ -1393,7 +1393,7 @@ void CegInstantiator::presolve( Node q ) { Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); lem = NodeManager::currentNM()->mkNode( OR, g, lem ); - Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; + Trace("cegqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; Assert(!expr::hasFreeVar(lem)); d_qe->getOutputChannel().lemma( lem, false, true ); } @@ -1401,7 +1401,7 @@ void CegInstantiator::presolve( Node q ) { } void CegInstantiator::processAssertions() { - Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() + Trace("cegqi-proc") << "--- Process assertions, #var = " << d_vars.size() << std::endl; d_curr_asserts.clear(); d_curr_eqc.clear(); @@ -1414,12 +1414,12 @@ void CegInstantiator::processAssertions() { for( unsigned i=0; ihasTerm( pv ) ){ Node pvr = ee->getRepresentative( pv ); if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){ - Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl; + Trace("cegqi-proc") << "Collect equivalence class " << pvr << std::endl; eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); while( !eqc_i.isFinished() ){ d_curr_eqc[pvr].push_back( *eqc_i ); @@ -1433,7 +1433,7 @@ void CegInstantiator::processAssertions() { TheoryId tid = d_tids[i]; Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){ - Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl; + Trace("cegqi-proc") << "Collect assertions from theory " << tid << std::endl; d_curr_asserts[tid].clear(); //collect all assertions from theory for( context::CDList::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) { @@ -1441,15 +1441,15 @@ void CegInstantiator::processAssertions() { Node atom = lit.getKind()==NOT ? lit[0] : lit; if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){ d_curr_asserts[tid].push_back( lit ); - Trace("cbqi-proc-debug") << "...add : " << lit << std::endl; + Trace("cegqi-proc-debug") << "...add : " << lit << std::endl; }else{ - Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl; + Trace("cegqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl; } } } } //collect equivalence classes that correspond to relevant theories - Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl; + Trace("cegqi-proc-debug") << "...collect typed equivalence classes" << std::endl; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ Node r = *eqcs_i; @@ -1460,18 +1460,18 @@ void CegInstantiator::processAssertions() { if( rtn.isInteger() || rtn.isReal() ){ rtn = rtn.getBaseType(); } - Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl; + Trace("cegqi-proc-debug") << "...type eqc: " << r << std::endl; d_curr_type_eqc[rtn].push_back( r ); if( d_curr_eqc.find( r )==d_curr_eqc.end() ){ - Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl; - Trace("cbqi-proc-debug") << " "; + Trace("cegqi-proc") << "Collect equivalence class " << r << std::endl; + Trace("cegqi-proc-debug") << " "; eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( !eqc_i.isFinished() ){ - Trace("cbqi-proc-debug") << *eqc_i << " "; + Trace("cegqi-proc-debug") << *eqc_i << " "; d_curr_eqc[r].push_back( *eqc_i ); ++eqc_i; } - Trace("cbqi-proc-debug") << std::endl; + Trace("cegqi-proc-debug") << std::endl; } } ++eqcs_i; @@ -1486,13 +1486,13 @@ void CegInstantiator::processAssertions() { if( isEligible( n ) ){ //must contain at least one variable if( !d_prog_var[n].empty() ){ - Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl; + Trace("cegqi-proc") << "...literal[" << it->first << "] : " << n << std::endl; akeep.push_back( n ); }else{ - Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl; + Trace("cegqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl; } }else{ - Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl; + Trace("cegqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl; } } it->second.clear(); @@ -1564,7 +1564,7 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) } }else{ if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){ - Trace("cbqi-ce-atoms") << "CE atoms : " << n << std::endl; + Trace("cegqi-ce-atoms") << "CE atoms : " << n << std::endl; d_ce_atoms.push_back( n ); } } @@ -1572,7 +1572,7 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) } void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { - Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl; + Trace("cegqi-reg") << "Register counterexample lemma..." << std::endl; d_input_vars.clear(); d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end()); @@ -1581,12 +1581,12 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st registerTheoryId(THEORY_UF); for (unsigned i = 0; i < ce_vars.size(); i++) { - Trace("cbqi-reg") << " register input variable : " << ce_vars[i] << std::endl; + Trace("cegqi-reg") << " register input variable : " << ce_vars[i] << std::endl; registerVariable(ce_vars[i]); } // preprocess with all relevant instantiator preprocessors - Trace("cbqi-debug") << "Preprocess based on theory-specific methods..." + Trace("cegqi-debug") << "Preprocess based on theory-specific methods..." << std::endl; std::vector pvars; pvars.insert(pvars.end(), d_vars.begin(), d_vars.end()); @@ -1595,12 +1595,12 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st p.second->registerCounterexampleLemma(lems, pvars); } // must register variables generated by preprocessors - Trace("cbqi-debug") << "Register variables from theory-specific methods " + Trace("cegqi-debug") << "Register variables from theory-specific methods " << d_input_vars.size() << " " << pvars.size() << " ..." << std::endl; for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i) { - Trace("cbqi-reg") << " register theory preprocess variable : " << pvars[i] + Trace("cegqi-reg") << " register theory preprocess variable : " << pvars[i] << std::endl; registerVariable(pvars[i]); } @@ -1609,21 +1609,21 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st IteSkolemMap iteSkolemMap; d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap); for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { - Trace("cbqi-reg") << " register aux variable : " << i->first << std::endl; + Trace("cegqi-reg") << " register aux variable : " << i->first << std::endl; registerVariable(i->first); } for( unsigned i=0; igetTheoryEngine()->preprocess(rlem); - Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; + Trace("cegqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; lems[i] = rlem; } // determine variable order: must do Reals before Ints - Trace("cbqi-debug") << "Determine variable order..." << std::endl; + Trace("cegqi-debug") << "Determine variable order..." << std::endl; if (!d_vars.empty()) { std::map voo; @@ -1647,21 +1647,21 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } if (doSort) { - Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl; + Trace("cegqi-debug") << "Sort variables based on ordering." << std::endl; for (std::pair >& vs : tvars) { vars.insert(vars.end(), vs.second.begin(), vs.second.end()); } - Trace("cbqi-debug") << "Consider variables in this order : " << std::endl; + Trace("cegqi-debug") << "Consider variables in this order : " << std::endl; for (unsigned i = 0; i < vars.size(); i++) { d_var_order_index[voo[vars[i]]] = i; - Trace("cbqi-debug") << " " << vars[i] << " : " << vars[i].getType() + Trace("cegqi-debug") << " " << vars[i] << " : " << vars[i].getType() << ", index was : " << voo[vars[i]] << std::endl; d_vars[i] = vars[i]; } - Trace("cbqi-debug") << std::endl; + Trace("cegqi-debug") << std::endl; } else { diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 8273f2c91..208eb0bf8 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -66,7 +66,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) d_small_const = NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000)); d_check_vts_lemma_lc = false; - if (options::cbqiBv()) + if (options::cegqiBv()) { // if doing instantiation for BV, need the inverter class d_bv_invert.reset(new quantifiers::BvInverter); @@ -96,7 +96,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) if( !hasAddedCbqiLemma( q ) ){ NodeManager* nm = NodeManager::currentNM(); d_added_cbqi_lemma.insert( q ); - Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; + Trace("cegqi-debug") << "Do cbqi for " << q << std::endl; //add cbqi lemma //get the counterexample literal Node ceLit = getCounterexampleLiteral(q); @@ -106,10 +106,10 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); //require any decision on cel to be phase=true d_quantEngine->addRequirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl; //add counterexample lemma lem = Rewriter::rewrite( lem ); - Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl; + Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; registerCounterexampleLemma( q, lem ); //totality lemmas for EPR @@ -129,7 +129,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) disj.push_back( ic.eqNode( itc->second[j] ) ); } Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); - Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl; + Trace("cegqi-lemma") << "EPR totality lemma : " << tlem << std::endl; d_quantEngine->getOutputChannel().lemma( tlem ); }else{ Assert(false); @@ -162,7 +162,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) if (!dep.empty()) { Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep)); - Trace("cbqi-lemma") + Trace("cegqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; d_quantEngine->getOutputChannel().lemma(dep_lemma); } @@ -174,14 +174,14 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) if( doCbqi( quants[i] ) ){ registerCbqiLemma( quants[i] ); } - if( options::cbqiNestedQE() ){ + if( options::cegqiNestedQE() ){ //record these as counterexample quantifiers QAttributes qa; QuantAttributes::computeQuantAttributes( quants[i], qa ); if( !qa.d_qid_num.isNull() ){ d_id_to_ce_quant[ qa.d_qid_num ] = quants[i]; d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num; - Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl; + Trace("cegqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl; } } } @@ -226,21 +226,21 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) Assert(hasAddedCbqiLemma(q)); if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ d_active_quant[q] = true; - Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; + Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl; Node cel = getCounterexampleLiteral(q); bool value; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; + Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl; if( !value ){ if( d_quantEngine->getValuation().isDecision( cel ) ){ - Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; + Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; }else{ - Trace("cbqi") << "Inactive : " << q << std::endl; + Trace("cegqi") << "Inactive : " << q << std::endl; d_quantEngine->getModel()->setQuantifierActive( q, false ); d_cbqi_set_quant_inactive = true; d_active_quant.erase( q ); d_elim_quants.insert( q ); - Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl; + Trace("cegqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl; //process from waitlist while( d_nested_qe_waitlist_proc[q]getOutputChannel().lemma( dqelem ); d_nested_qe_waitlist_proc[q] = index + 1; } } } }else{ - Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; + Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl; } } } } //refinement: only consider innermost active quantified formulas - if( options::cbqiInnermost() ){ + if( options::cegqiInnermost() ){ if( !d_children_quant.empty() && !d_active_quant.empty() ){ - Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl; + Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl; std::vector< Node > ninner; for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first ); if( itc!=d_children_quant.end() ){ for( unsigned j=0; jsecond.size(); j++ ){ if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){ - Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl; + Trace("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl; ninner.push_back( it->first ); break; } } } } - Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; + Trace("cegqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; for( unsigned i=0; iinConflict()); double clSet = 0; - if( Trace.isOn("cbqi-engine") ){ + if( Trace.isOn("cegqi-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); - Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; + Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; } unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); for( int ee=0; ee<=1; ee++ ){ @@ -308,14 +308,14 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) // if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ Node q = it->first; - Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; + Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; if( d_nested_qe.find( q )==d_nested_qe.end() ){ process( q, e, ee ); if( d_quantEngine->inConflict() ){ break; } }else{ - Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; + Trace("cegqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; Assert(false); } } @@ -323,19 +323,19 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) break; } } - if( Trace.isOn("cbqi-engine") ){ + if( Trace.isOn("cegqi-engine") ){ if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ - Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; + Trace("cegqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; } double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; + Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; } } } bool InstStrategyCegqi::checkComplete() { - if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ + if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ return false; }else{ return true; @@ -415,7 +415,7 @@ void InstStrategyCegqi::checkOwnership(Node q) void InstStrategyCegqi::preRegisterQuantifier(Node q) { // mark all nested quantifiers with id - if (options::cbqiNestedQE()) + if (options::cegqiNestedQE()) { if( d_quantEngine->getOwner(q)==this ) { @@ -436,20 +436,20 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q) } Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc); Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq); - Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl; + Trace("cegqi-lemma") << "Mark quant id lemma : " << mlem << std::endl; d_quantEngine->addLemma(mlem); } } } if( doCbqi( q ) ){ // get the instantiator - if (options::cbqiPreRegInst()) + if (options::cegqiPreRegInst()) { getInstantiator(q); } // register the cbqi lemma if( registerCbqiLemma( q ) ){ - Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; + Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; } } } @@ -466,7 +466,7 @@ Node InstStrategyCegqi::rewriteInstantiation(Node q, inst = d_vtsCache->rewriteVtsSymbols(inst); Trace("quant-vts-debug") << "...got " << inst << std::endl; } - if (options::cbqiNestedQE()) + if (options::cegqiNestedQE()) { inst = doNestedQE(q, terms, inst, doVts); } @@ -488,9 +488,9 @@ Node InstStrategyCegqi::doNestedQENode( // in this case, q is equivalent to the quantifier-free formula C[t]. if( d_nested_qe.find( ceq )==d_nested_qe.end() ){ d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq ); - Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl; - Trace("cbqi-nqe") << " " << ceq << std::endl; - Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl; + Trace("cegqi-nqe") << "CE quantifier elimination : " << std::endl; + Trace("cegqi-nqe") << " " << ceq << std::endl; + Trace("cegqi-nqe") << " " << d_nested_qe[ceq] << std::endl; //should not contain quantifiers Assert(!expr::hasClosure(d_nested_qe[ceq])); } @@ -505,9 +505,9 @@ Node InstStrategyCegqi::doNestedQENode( ret = Rewriter::rewrite( ret ); ret = d_vtsCache->rewriteVtsSymbols(ret); } - Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; - Trace("cbqi-nqe") << " " << n << std::endl; - Trace("cbqi-nqe") << " " << ret << std::endl; + Trace("cegqi-nqe") << "Nested quantifier elimination: " << std::endl; + Trace("cegqi-nqe") << " " << n << std::endl; + Trace("cegqi-nqe") << " " << ret << std::endl; return ret; } @@ -531,10 +531,10 @@ Node InstStrategyCegqi::doNestedQERec(Node q, if( doNestedQe ){ ret = doNestedQENode( q, ceq, n, inst_terms, doVts ); }else{ - Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl; + Trace("cegqi-nqe") << "Add to nested qe waitlist : " << std::endl; Node nr = Rewriter::rewrite( n ); - Trace("cbqi-nqe") << " " << ceq << std::endl; - Trace("cbqi-nqe") << " " << nr << std::endl; + Trace("cegqi-nqe") << " " << ceq << std::endl; + Trace("cegqi-nqe") << " " << nr << std::endl; int wlsize = d_nested_qe_waitlist_size[ceq] + 1; d_nested_qe_waitlist_size[ceq] = wlsize; if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){ @@ -547,7 +547,7 @@ Node InstStrategyCegqi::doNestedQERec(Node q, d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() ); d_nested_qe_info[nr].d_doVts = doVts; //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true. - Assert(!options::cbqiInnermost()); + Assert(!options::cegqiInnermost()); } } } @@ -599,7 +599,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) cinst->registerCounterexampleLemma(lems, ce_vars); for (unsigned i = 0, size = lems.size(); i < size; i++) { - Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] + Trace("cegqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl; d_quantEngine->addLemma(lems[i], false); } @@ -610,7 +610,7 @@ bool InstStrategyCegqi::doCbqi(Node q) std::map::iterator it = d_do_cbqi.find(q); if( it==d_do_cbqi.end() ){ CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine); - Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; + Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; return ret != CEG_UNHANDLED; } @@ -687,7 +687,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { return true; }else{ //this should never happen for monotonic selection strategies - Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl; + Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl; return false; } } @@ -719,13 +719,13 @@ BvInverter* InstStrategyCegqi::getBvInverter() const } void InstStrategyCegqi::presolve() { - if (!options::cbqiPreRegInst()) + if (!options::cegqiPreRegInst()) { return; } for (std::pair>& ci : d_cinst) { - Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl; + Trace("cegqi-presolve") << "Presolve " << ci.first << std::endl; ci.second->presolve(ci.first); } } diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index ee6291564..784453838 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -31,7 +31,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; bool CandidateGenerator::isLegalCandidate( Node n ){ - return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); + return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); } CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat) diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 964d2e492..a95944bed 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -1053,7 +1053,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q, Assert(Trigger::isSimpleTrigger(d_match_pattern)); for( unsigned i=0; igetTypeGroundTerm(ftypes[i], j); - if (!options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) + if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) { Node rep = qy->getRepresentative(gt); if (reps_found.find(rep) == reps_found.end()) diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 218753308..89e2678fc 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -146,7 +146,7 @@ bool Instantiate::addInstantiation( << std::endl; bad_inst = true; } - else if (options::cbqi()) + else if (options::cegqi()) { Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]); if (!icf.isNull()) diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 511eb6d79..2d1cf6531 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1925,7 +1925,7 @@ void QuantConflictFind::reset_round( Theory::Effort level ) { if (tdb->hasTermCurrent(r)) { TypeNode rtn = r.getType(); - if (!options::cbqi() || !TermUtil::hasInstConstAttr(r)) + if (!options::cegqi() || !TermUtil::hasInstConstAttr(r)) { d_eqcs[rtn].push_back(r); } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 27d77dfbb..ec1b9e71a 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -56,7 +56,7 @@ void CegSingleInv::initialize(Node q) Assert(d_quant.isNull()); d_quant = q; d_simp_quant = q; - Trace("cegqi-si") << "CegSingleInv::initialize : " << q << std::endl; + Trace("sygus-si") << "CegSingleInv::initialize : " << q << std::endl; // infer single invocation-ness // get the variables @@ -87,13 +87,13 @@ void CegSingleInv::initialize(Node q) // process the single invocation-ness of the property if (!d_sip->init(progs, qq)) { - Trace("cegqi-si") << "...not single invocation (type mismatch)" + Trace("sygus-si") << "...not single invocation (type mismatch)" << std::endl; return; } - Trace("cegqi-si") << "- Partitioned to single invocation parts : " + Trace("sygus-si") << "- Partitioned to single invocation parts : " << std::endl; - d_sip->debugPrint("cegqi-si"); + d_sip->debugPrint("sygus-si"); // map from program to bound variables std::vector funcs; @@ -142,7 +142,7 @@ void CegSingleInv::initialize(Node q) return; } // if we are doing invariant templates, then construct the template - Trace("cegqi-si") << "- Do transition inference..." << std::endl; + Trace("sygus-si") << "- Do transition inference..." << std::endl; d_ti[q].process(qq, q[0][0]); Trace("cegqi-inv") << std::endl; Node prog = d_ti[q].getFunction(); @@ -194,7 +194,7 @@ void CegSingleInv::initialize(Node q) .negate(); d_simp_quant = Rewriter::rewrite(d_simp_quant); d_simp_quant = nm->mkNode(FORALL, q[0], d_simp_quant, q[2]); - Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl; + Trace("sygus-si") << "Rewritten quantifier : " << d_simp_quant << std::endl; // construct template argument d_templ_arg[prog] = nm->mkSkolem("I", invariant.getType()); @@ -273,21 +273,21 @@ void CegSingleInv::initialize(Node q) void CegSingleInv::finishInit(bool syntaxRestricted) { - Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl; + Trace("sygus-si-debug") << "Single invocation: finish init" << std::endl; // do not do single invocation if grammar is restricted and // options::CegqiSingleInvMode::ALL is not enabled if (options::cegqiSingleInvMode() == options::CegqiSingleInvMode::USE && d_single_invocation && syntaxRestricted) { d_single_invocation = false; - Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl; + Trace("sygus-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl; } // we now have determined whether we will do single invocation techniques if (!d_single_invocation) { d_single_inv = Node::null(); - Trace("cegqi-si") << "Formula is not single invocation." << std::endl; + Trace("sygus-si") << "Formula is not single invocation." << std::endl; if (options::cegqiSingleInvAbort()) { std::stringstream ss; @@ -320,7 +320,7 @@ void CegSingleInv::finishInit(bool syntaxRestricted) sivars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end()); - Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv + Trace("sygus-si") << "Single invocation formula is : " << d_single_inv << std::endl; // check whether we can handle this quantified formula CegHandledStatus status = CEG_HANDLED; @@ -332,10 +332,10 @@ void CegSingleInv::finishInit(bool syntaxRestricted) status = CegInstantiator::isCbqiQuant(d_single_inv); } } - Trace("cegqi-si") << "CegHandledStatus is " << status << std::endl; + Trace("sygus-si") << "CegHandledStatus is " << status << std::endl; if (status < CEG_HANDLED) { - Trace("cegqi-si") << "...do not invoke single invocation techniques since " + Trace("sygus-si") << "...do not invoke single invocation techniques since " "the quantified formula does not have a handled " "counterexample-guided instantiation strategy!" << std::endl; @@ -356,7 +356,7 @@ bool CegSingleInv::solve() // already solved, probably via a call to solveTrivial. return true; } - Trace("cegqi-si") << "Solve using single invocation..." << std::endl; + Trace("sygus-si") << "Solve using single invocation..." << std::endl; NodeManager* nm = NodeManager::currentNM(); // Mark the quantified formula with the quantifier elimination attribute to // ensure its structure is preserved in the query below. @@ -378,7 +378,7 @@ bool CegSingleInv::solve() siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); siSmt.assertFormula(siq.toExpr()); Result r = siSmt.checkSat(); - Trace("cegqi-si") << "Result: " << r << std::endl; + Trace("sygus-si") << "Result: " << r << std::endl; if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) { // conjecture is infeasible or unknown @@ -389,7 +389,7 @@ bool CegSingleInv::solve() siSmt.getInstantiatedQuantifiedFormulas(qs); Assert(qs.size() <= 1); // track the instantiations, as solution construction is based on this - Trace("cegqi-si") << "#instantiated quantified formulas=" << qs.size() + Trace("sygus-si") << "#instantiated quantified formulas=" << qs.size() << std::endl; d_inst.clear(); d_instConds.clear(); @@ -399,7 +399,7 @@ bool CegSingleInv::solve() Assert(qn.getKind() == FORALL); std::vector > tvecs; siSmt.getInstantiationTermVectors(q, tvecs); - Trace("cegqi-si") << "#instantiations of " << q << "=" << tvecs.size() + Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size() << std::endl; std::vector vars; for (const Node& v : qn[0]) @@ -415,14 +415,14 @@ bool CegSingleInv::solve() { inst.push_back(Node::fromExpr(t)); } - Trace("cegqi-si") << " Instantiation: " << inst << std::endl; + Trace("sygus-si") << " Instantiation: " << inst << std::endl; d_inst.push_back(inst); Assert(inst.size() == vars.size()); Node ilem = body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end()); ilem = Rewriter::rewrite(ilem); d_instConds.push_back(ilem); - Trace("cegqi-si") << " Instantiation Lemma: " << ilem << std::endl; + Trace("sygus-si") << " Instantiation Lemma: " << ilem << std::endl; } } d_isSolved = true; @@ -654,7 +654,7 @@ bool CegSingleInv::solveTrivial(Node q) // if we solved all arguments if (args.empty() && body.isConst() && !body.getConst()) { - Trace("cegqi-si-trivial-solve") + Trace("sygus-si-trivial-solve") << q << " is trivially solvable by substitution " << vars << " -> " << subs << std::endl; std::map imap; @@ -673,7 +673,7 @@ bool CegSingleInv::solveTrivial(Node q) d_isSolved = true; return true; } - Trace("cegqi-si-trivial-solve") + Trace("sygus-si-trivial-solve") << q << " is not trivially solvable." << std::endl; return false; } diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index dfef0bad4..0c11baecc 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -138,7 +138,7 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, // constructors. if (!d_usingSymCons) { - Trace("cegqi-engine") << " *** Do refinement lemma evaluation" + Trace("sygus-engine") << " *** Do refinement lemma evaluation" << (doGen ? " with conjecture-specific refinement" : "") << "..." << std::endl; @@ -168,7 +168,7 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, // just check whether the refinement lemmas are satisfied, fail if not if (checkRefinementEvalLemmas(candidates, candidate_values)) { - Trace("cegqi-engine") << "...(actively enumerated) candidate failed " + Trace("sygus-engine") << "...(actively enumerated) candidate failed " "refinement lemma evaluation." << std::endl; return true; @@ -179,7 +179,7 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons; if (doEvalUnfold) { - Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl; + Trace("sygus-engine") << " *** Do evaluation unfolding..." << std::endl; std::vector eager_terms, eager_vals, eager_exps; for (unsigned i = 0, size = candidates.size(); i < size; ++i) { @@ -627,7 +627,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, const std::vector& vals, std::vector& lems) { - Trace("cegqi-engine") << " *** Do sample add refinement..." << std::endl; + Trace("sygus-engine") << " *** Do sample add refinement..." << std::endl; if (Trace.isOn("cegis-sample")) { Trace("cegis-sample") << "Check sampling for candidate solution" @@ -681,7 +681,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, } Trace("cegis-sample") << std::endl; } - Trace("cegqi-engine") << " *** Refine by sampling" << std::endl; + Trace("sygus-engine") << " *** Refine by sampling" << std::endl; addRefinementLemma(rlem); // if trust, we are not interested in sending out refinement lemmas if (options::cegisSample() != options::CegisSampleMode::TRUST) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 3590e76f1..ce3c94914 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -781,7 +781,7 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() } if (doTerminate) { - Trace("cegqi-engine") << "master(" << d_tn << "): complete at size " + Trace("sygus-engine") << "master(" << d_tn << "): complete at size " << d_currSize << std::endl; tc.setComplete(); return false; @@ -793,12 +793,12 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() d_currSize++; Trace("sygus-enum-debug2") << "master(" << d_tn << "): size++ : " << d_currSize << "\n"; - if (Trace.isOn("cegqi-engine")) + if (Trace.isOn("sygus-engine")) { // am i the master enumerator? if so, print if (d_se->d_tlEnum == this) { - Trace("cegqi-engine") << "SygusEnumerator::size = " << d_currSize + Trace("sygus-engine") << "SygusEnumerator::size = " << d_currSize << std::endl; } } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index df41672e2..aa0dc8e5e 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -256,7 +256,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, } } - Trace("cegqi-engine") << "Repairing previous solution..." << std::endl; + Trace("sygus-engine") << "Repairing previous solution..." << std::endl; // make the satisfiability query bool needExport = true; ExprManagerMapCollection varMap; @@ -268,7 +268,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, if (r.asSatisfiabilityResult().isSat() == Result::UNSAT || r.asSatisfiabilityResult().isUnknown()) { - Trace("cegqi-engine") << "...failed" << std::endl; + Trace("sygus-engine") << "...failed" << std::endl; return false; } std::vector sk_sygus_m; @@ -300,7 +300,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, Node scsk = csk.substitute( sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end()); repair_cv.push_back(scsk); - if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine")) + if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine")) { std::stringstream sss; Printer::getPrinter(options::outputLanguage()) @@ -308,8 +308,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody, ss << " * " << candidates[i] << " -> " << sss.str() << std::endl; } } - Trace("cegqi-engine") << "...success:" << std::endl; - Trace("cegqi-engine") << ss.str(); + Trace("sygus-engine") << "...success:" << std::endl; + Trace("sygus-engine") << ss.str(); Trace("sygus-repair-const") << "Repaired constants in solution : " << std::endl; Trace("sygus-repair-const") << ss.str(); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e69d746fe..bb5307c79 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -280,12 +280,12 @@ bool SynthConjecture::needsCheck() { if (!value) { - Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; + Trace("sygus-engine-debug") << "Conjecture is infeasible." << std::endl; return false; } else { - Trace("cegqi-engine-debug") << "Feasible guard " << d_feasible_guard + Trace("sygus-engine-debug") << "Feasible guard " << d_feasible_guard << " assigned true." << std::endl; } } @@ -366,16 +366,16 @@ bool SynthConjecture::doCheck(std::vector& lems) Assert(d_repair_index < d_cinfo[cprog].d_inst.size()); fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]); } - if (Trace.isOn("cegqi-engine")) + if (Trace.isOn("sygus-engine")) { - Trace("cegqi-engine") << "CegConjuncture : repair previous solution "; + Trace("sygus-engine") << "CegConjuncture : repair previous solution "; for (const Node& fc : fail_cvs) { std::stringstream ss; Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc); - Trace("cegqi-engine") << ss.str() << " "; + Trace("sygus-engine") << ss.str() << " "; } - Trace("cegqi-engine") << std::endl; + Trace("sygus-engine") << std::endl; } d_repair_index++; if (d_sygus_rconst->repairSolution( @@ -397,7 +397,7 @@ bool SynthConjecture::doCheck(std::vector& lems) if (!d_master->allowPartialModel() && !fullModel) { // we retain the values in d_ev_active_gen_waiting - Trace("cegqi-engine-debug") << "...partial model, fail." << std::endl; + Trace("sygus-engine-debug") << "...partial model, fail." << std::endl; // if we are partial due to an active enumerator, we may still succeed // on the next call return !activeIncomplete; @@ -416,13 +416,13 @@ bool SynthConjecture::doCheck(std::vector& lems) } if (emptyModel) { - Trace("cegqi-engine-debug") << "...empty model, fail." << std::endl; + Trace("sygus-engine-debug") << "...empty model, fail." << std::endl; return !activeIncomplete; } // debug print - if (Trace.isOn("cegqi-engine")) + if (Trace.isOn("sygus-engine")) { - Trace("cegqi-engine") << " * Value is : "; + Trace("sygus-engine") << " * Value is : "; for (unsigned i = 0, size = terms.size(); i < size; i++) { Node nv = enum_values[i]; @@ -430,23 +430,23 @@ bool SynthConjecture::doCheck(std::vector& lems) TypeNode tn = onv.getType(); std::stringstream ss; Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv); - Trace("cegqi-engine") << terms[i] << " -> "; + Trace("sygus-engine") << terms[i] << " -> "; if (nv.isNull()) { - Trace("cegqi-engine") << "[EXC: " << ss.str() << "] "; + Trace("sygus-engine") << "[EXC: " << ss.str() << "] "; } else { - Trace("cegqi-engine") << ss.str() << " "; - if (Trace.isOn("cegqi-engine-rr")) + Trace("sygus-engine") << ss.str() << " "; + if (Trace.isOn("sygus-engine-rr")) { Node bv = d_tds->sygusToBuiltin(nv, tn); bv = Rewriter::rewrite(bv); - Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + Trace("sygus-engine-rr") << " -> " << bv << std::endl; } } } - Trace("cegqi-engine") << std::endl; + Trace("sygus-engine") << std::endl; } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( @@ -471,7 +471,7 @@ bool SynthConjecture::doCheck(std::vector& lems) if (!checkSideCondition(candidate_values)) { excludeCurrentSolution(terms, candidate_values); - Trace("cegqi-engine") << "...failed side condition" << std::endl; + Trace("sygus-engine") << "...failed side condition" << std::endl; return false; } } @@ -590,22 +590,22 @@ bool SynthConjecture::doCheck(std::vector& lems) lem = nm->mkNode(OR, d_quant.negate(), query); if (options::sygusVerifySubcall()) { - Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl; + Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; Result r = checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs); - Trace("cegqi-engine") << " ...got " << r << std::endl; + Trace("sygus-engine") << " ...got " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::SAT) { - if (Trace.isOn("cegqi-engine")) + if (Trace.isOn("sygus-engine")) { - Trace("cegqi-engine") << " * Verification lemma failed for:\n "; + Trace("sygus-engine") << " * Verification lemma failed for:\n "; for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) { - Trace("cegqi-engine") + Trace("sygus-engine") << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " "; } - Trace("cegqi-engine") << std::endl; + Trace("sygus-engine") << std::endl; } #ifdef CVC4_ASSERTIONS // the values for the query should be a complete model @@ -658,7 +658,7 @@ bool SynthConjecture::checkSideCondition(const std::vector& cvals) const { Node sc = d_embedSideCondition.substitute( d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end()); - Trace("cegqi-engine") << "Check side condition..." << std::endl; + Trace("sygus-engine") << "Check side condition..." << std::endl; Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; Result r = checkWithSubsolver(sc); Trace("cegqi-debug") << "...got side condition : " << r << std::endl; @@ -666,7 +666,7 @@ bool SynthConjecture::checkSideCondition(const std::vector& cvals) const { return false; } - Trace("cegqi-engine") << "...passed side condition" << std::endl; + Trace("sygus-engine") << "...passed side condition" << std::endl; } return true; } @@ -763,7 +763,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector& n, Node gstatus = d_qe->getValuation().getSatValue(g); if (gstatus.isNull() || !gstatus.getConst()) { - Trace("cegqi-engine-debug") + Trace("sygus-engine-debug") << "Enumerator " << e << " is inactive." << std::endl; continue; } @@ -785,7 +785,7 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) // if the current model value of e was not registered by the datatypes // sygus solver, or was excluded by symmetry breaking, then it does not // have a proper model value that we should consider, thus we return null. - Trace("cegqi-engine-debug") + Trace("sygus-engine-debug") << "Enumerator " << e << " does not have proper model value." << std::endl; return Node::null(); diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 0c8b8f734..b0a562b42 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -43,12 +43,12 @@ SynthEngine::~SynthEngine() {} void SynthEngine::presolve() { - Trace("cegqi-engine") << "SynthEngine::presolve" << std::endl; + Trace("sygus-engine") << "SynthEngine::presolve" << std::endl; for (unsigned i = 0, size = d_conjs.size(); i < size; i++) { d_conjs[i]->presolve(); } - Trace("cegqi-engine") << "SynthEngine::presolve finished" << std::endl; + Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl; } bool SynthEngine::needsCheck(Theory::Effort e) @@ -75,7 +75,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) { Node q = d_waiting_conj.back(); d_waiting_conj.pop_back(); - Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q + Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q << std::endl; assignConjecture(q); } @@ -87,9 +87,9 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) return; } - Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" + Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; - Trace("cegqi-engine-debug") << std::endl; + Trace("sygus-engine-debug") << std::endl; Valuation& valuation = d_quantEngine->getValuation(); std::vector activeCheckConj; for (unsigned i = 0, size = d_conjs.size(); i < size; i++) @@ -103,10 +103,10 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) } else { - Trace("cegqi-engine-debug") << "...no value for quantified formula." + Trace("sygus-engine-debug") << "...no value for quantified formula." << std::endl; } - Trace("cegqi-engine-debug") + Trace("sygus-engine-debug") << "Current conjecture status : active : " << active << std::endl; if (active && sc->needsCheck()) { @@ -116,7 +116,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) std::vector acnext; do { - Trace("cegqi-engine-debug") << "Checking " << activeCheckConj.size() + Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size() << " active conjectures..." << std::endl; for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++) { @@ -134,13 +134,13 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) acnext.clear(); } while (!activeCheckConj.empty() && !d_quantEngine->theoryEngineNeedsCheck()); - Trace("cegqi-engine") + Trace("sygus-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; } void SynthEngine::assignConjecture(Node q) { - Trace("cegqi-engine") << "SynthEngine::assignConjecture " << q << std::endl; + Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl; if (options::sygusQePreproc()) { // the following does quantifier elimination as a preprocess step @@ -307,16 +307,16 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) { Node q = conj->getEmbeddedConjecture(); Node aq = conj->getConjecture(); - if (Trace.isOn("cegqi-engine-debug")) + if (Trace.isOn("sygus-engine-debug")) { - conj->debugPrint("cegqi-engine-debug"); - Trace("cegqi-engine-debug") << std::endl; + conj->debugPrint("sygus-engine-debug"); + Trace("sygus-engine-debug") << std::endl; } if (!conj->needsRefinement()) { - Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; - Trace("cegqi-engine-debug") + Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl; + Trace("sygus-engine-debug") << " *** Check candidate phase..." << std::endl; std::vector cclems; bool ret = conj->doCheck(cclems); @@ -331,13 +331,13 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) else { // this may happen if we eagerly unfold, simplify to true - Trace("cegqi-engine-debug") + Trace("sygus-engine-debug") << " ...FAILED to add candidate!" << std::endl; } } if (addedLemma) { - Trace("cegqi-engine-debug") + Trace("sygus-engine-debug") << " ...check for counterexample." << std::endl; return true; } @@ -353,7 +353,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) } else { - Trace("cegqi-engine-debug") + Trace("sygus-engine-debug") << " *** Refine candidate phase..." << std::endl; std::vector rlems; conj->doRefine(rlems); @@ -377,7 +377,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) } if (addedLemma) { - Trace("cegqi-engine-debug") << " ...refine candidate." << std::endl; + Trace("sygus-engine-debug") << " ...refine candidate." << std::endl; } } return true; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e4caaa539..ca4768ee4 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -118,7 +118,7 @@ class QuantifiersEnginePrivate d_inst_engine.reset(new quantifiers::InstantiationEngine(qe)); modules.push_back(d_inst_engine.get()); } - if (options::cbqi()) + if (options::cegqi()) { d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe)); modules.push_back(d_i_cbqi.get()); diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy index 02879cb8d..592189df2 100644 --- a/test/regress/regress0/expect/scrub.08.sy +++ b/test/regress/regress0/expect/scrub.08.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --no-sygus-repair-const +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --no-sygus-repair-const ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM diff --git a/test/regress/regress0/quantifiers/ari056.smt2 b/test/regress/regress0/quantifiers/ari056.smt2 index a1f4aef04..aee3cd970 100644 --- a/test/regress/regress0/quantifiers/ari056.smt2 +++ b/test/regress/regress0/quantifiers/ari056.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi +; COMMAND-LINE: --cegqi ; EXPECT: unsat (set-logic UFNIRA) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 index fe567f898..7e58ea87c 100644 --- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 +++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi --dt-rewrite-error-sel --lang=smt2.5 +; COMMAND-LINE: --cegqi --dt-rewrite-error-sel --lang=smt2.5 ; EXPECT: unsat (set-logic ALL_SUPPORTED) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/quantifiers/issue4086-infs.smt2 b/test/regress/regress0/quantifiers/issue4086-infs.smt2 index 2ebb45960..faad2cf18 100644 --- a/test/regress/regress0/quantifiers/issue4086-infs.smt2 +++ b/test/regress/regress0/quantifiers/issue4086-infs.smt2 @@ -1,7 +1,7 @@ (set-logic LIRA) (set-info :status unsat) -(set-option :cbqi-use-inf-int true) -(set-option :cbqi-use-inf-real true) +(set-option :cegqi-use-inf-int true) +(set-option :cegqi-use-inf-real true) (set-option :var-ineq-elim-quant false) (assert (forall (( b Real )) (forall (( c Int )) (and (> c (* b 2 )))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 b/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 index 51d3e89ea..6caa2b10c 100644 --- a/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 +++ b/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 @@ -1,5 +1,5 @@ (set-logic UFBV) -(set-option :cbqi-all true) +(set-option :cegqi-all true) (set-info :status unsat) (declare-sort S0 0) (declare-const S0-0 S0) diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 index e75591dec..fd7b3f574 100644 --- a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 +++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi --finite-model-find --no-check-models +; COMMAND-LINE: --cegqi --finite-model-find --no-check-models ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 index b196ee262..efac3468c 100644 --- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 +++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi --no-check-models +; COMMAND-LINE: --cegqi --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 index 1486e176d..939918ef7 100644 --- a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 +++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 index 3c4f93243..b6095fcab 100644 --- a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 +++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2 index ec4626f52..2bdc2d994 100644 --- a/test/regress/regress0/quantifiers/qbv-simp.smt2 +++ b/test/regress/regress0/quantifiers/qbv-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --no-cegqi-full ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 index 216a98531..790918675 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 index ad3b9a9e5..ab1d665bb 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 index 8dd50b1be..80cc8db6d 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 index e05c3446d..92304674e 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 index 2835e5956..ea778697f 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 index 537f0ee3d..82efd63bf 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 index 1018ce72c..cd8d0db2d 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 index 503bc9852..9287e4c2b 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 index 74c2891cf..1758bbe38 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 index 4145c68b1..f5826fcda 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 index e85ecc7de..5fed3ada8 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 index abef84da2..d7bd29ba0 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 index a1dca469a..3d6aec051 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 index 4f9c6edc3..049df0b27 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 index 69c5def65..3dc095e83 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 index 769854f6f..4f8983e01 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 index 7b66bd859..81a299b4e 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 index 7dab5637e..ceda04f35 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 index 13fb3e1c2..d295cfcdc 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 index 43019c4cb..58b14a564 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy index 69bcd0f08..9dee4efdf 100755 --- a/test/regress/regress0/sygus/General_plus10.sy +++ b/test/regress/regress0/sygus/General_plus10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) (synth-fun fb () Int ((Start Int)) ((Start Int ((Constant Int))))) diff --git a/test/regress/regress0/sygus/aig-si.sy b/test/regress/regress0/sygus/aig-si.sy index 9330546d8..9d3af67fb 100644 --- a/test/regress/regress0/sygus/aig-si.sy +++ b/test/regress/regress0/sygus/aig-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi --cegqi-prereg-inst --sygus-out=status (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool diff --git a/test/regress/regress0/sygus/c100.sy b/test/regress/regress0/sygus/c100.sy index 994fb6de3..b0837e341 100644 --- a/test/regress/regress0/sygus/c100.sy +++ b/test/regress/regress0/sygus/c100.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/check-generic-red.sy b/test/regress/regress0/sygus/check-generic-red.sy index d593a7d9e..c1ebc52b2 100644 --- a/test/regress/regress0/sygus/check-generic-red.sy +++ b/test/regress/regress0/sygus/check-generic-red.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification (set-logic LIA) (synth-fun P ((x Int) (y Int)) Bool diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 31e88f523..78029cbc8 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy b/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy index b410e5d23..8c77eea61 100644 --- a/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy +++ b/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none ; EXPECT: unsat (set-logic BV) diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 9f9eea2a8..9793c927b 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status +; 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) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z))))))) diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index 91a865035..19a4e6bc9 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) (define-fun letf ((z Int)) Int (+ z z)) (synth-fun f ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy index 09fae5410..d3ca69e96 100644 --- a/test/regress/regress0/sygus/parity-AIG-d0.sy +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy index 99c308173..5bd6ebae4 100644 --- a/test/regress/regress0/sygus/pbe-pred-contra.sy +++ b/test/regress/regress0/sygus/pbe-pred-contra.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status ; EXPECT: unknown (set-logic LIA) (synth-fun P ((x Int)) Bool) diff --git a/test/regress/regress1/bug519.smt2 b/test/regress/regress1/bug519.smt2 index 6cabbaa64..2d7d3a9c5 100644 --- a/test/regress/regress1/bug519.smt2 +++ b/test/regress/regress1/bug519.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi -mi --no-check-models +; COMMAND-LINE: --cegqi -mi --no-check-models ; EXPECT: sat ; EXPECT: unsat diff --git a/test/regress/regress1/quantifiers/NUM878.smt2 b/test/regress/regress1/quantifiers/NUM878.smt2 index 8d78bf861..6f26e7af2 100644 --- a/test/regress/regress1/quantifiers/NUM878.smt2 +++ b/test/regress/regress1/quantifiers/NUM878.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cegqi-bv ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 b/test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 index 6379d6cec..e19532329 100644 --- a/test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 +++ b/test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-nested-qe +; COMMAND-LINE: --cegqi-nested-qe ; EXPECT: unsat (set-logic LRA) diff --git a/test/regress/regress1/quantifiers/anti-sk-simp.smt2 b/test/regress/regress1/quantifiers/anti-sk-simp.smt2 index 2ae54a075..a5f576f86 100644 --- a/test/regress/regress1/quantifiers/anti-sk-simp.smt2 +++ b/test/regress/regress1/quantifiers/anti-sk-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi --quant-anti-skolem +; COMMAND-LINE: --cegqi --quant-anti-skolem ; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2 b/test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2 index 2d70dfb8e..2372faa1e 100644 --- a/test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2 +++ b/test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cegqi-bv ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 b/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 index 4d5cf4ec4..cd921419c 100644 --- a/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 +++ b/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi --decision=internal +; COMMAND-LINE: --cegqi --decision=internal ; EXPECT: unsat (set-logic LIA) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/extract-nproc.smt2 b/test/regress/regress1/quantifiers/extract-nproc.smt2 index 6072776dc..30b6a300d 100644 --- a/test/regress/regress1/quantifiers/extract-nproc.smt2 +++ b/test/regress/regress1/quantifiers/extract-nproc.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-rm-extract +; COMMAND-LINE: --cegqi-bv --cegqi-bv-rm-extract ; EXPECT: sat (set-logic BV) (declare-fun k_3 () (_ BitVec 8)) diff --git a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 index 38a4ed127..fdbac9996 100644 --- a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 +++ b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cegqi-bv ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2 b/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2 index aa5cbc31e..92c8ac47b 100644 --- a/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2 +++ b/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2 @@ -3,7 +3,7 @@ (set-logic BV) (set-info :status sat) (declare-fun _substvar_16_ () Bool) -(set-option :cbqi-prereg-inst true) +(set-option :cegqi-prereg-inst true) (set-option :check-models true) (declare-fun v2 () Bool) (push 1) diff --git a/test/regress/regress1/quantifiers/lra-vts-inf.smt2 b/test/regress/regress1/quantifiers/lra-vts-inf.smt2 index 22d6455fb..80315edaf 100644 --- a/test/regress/regress1/quantifiers/lra-vts-inf.smt2 +++ b/test/regress/regress1/quantifiers/lra-vts-inf.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-use-inf-int --cbqi-use-inf-real +; COMMAND-LINE: --cegqi-use-inf-int --cegqi-use-inf-real ; EXPECT: unsat (set-info :smt-lib-version 2.6) (set-logic LRA) diff --git a/test/regress/regress1/quantifiers/model_6_1_bv.smt2 b/test/regress/regress1/quantifiers/model_6_1_bv.smt2 index 011430bd6..f2b69974f 100644 --- a/test/regress/regress1/quantifiers/model_6_1_bv.smt2 +++ b/test/regress/regress1/quantifiers/model_6_1_bv.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-nested-qe +; COMMAND-LINE: --cegqi-nested-qe ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 index 2a46d2a21..d39ad79f4 100644 --- a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 +++ b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cegqi-bv ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/regress1/quantifiers/nl-pow-trick.smt2 index 5152b89c4..82857c50a 100644 --- a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 +++ b/test/regress/regress1/quantifiers/nl-pow-trick.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-all --no-relational-triggers +; COMMAND-LINE: --cegqi-all --no-relational-triggers ; EXPECT: unsat (set-logic NIA) (declare-fun a () Int) diff --git a/test/regress/regress1/quantifiers/nra-interleave-inst.smt2 b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2 index 7d981597a..b01860f73 100644 --- a/test/regress/regress1/quantifiers/nra-interleave-inst.smt2 +++ b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-multi-inst +; COMMAND-LINE: --cegqi-multi-inst ; EXPECT: unsat (set-info :smt-lib-version 2.6) (set-logic NRA) diff --git a/test/regress/regress1/quantifiers/psyco-107-bv.smt2 b/test/regress/regress1/quantifiers/psyco-107-bv.smt2 index 82b54a231..06cec17c1 100644 --- a/test/regress/regress1/quantifiers/psyco-107-bv.smt2 +++ b/test/regress/regress1/quantifiers/psyco-107-bv.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=eq-boundary +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=eq-boundary ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/qbv-disequality3.smt2 b/test/regress/regress1/quantifiers/qbv-disequality3.smt2 index d16157509..78f5b7c88 100644 --- a/test/regress/regress1/quantifiers/qbv-disequality3.smt2 +++ b/test/regress/regress1/quantifiers/qbv-disequality3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 index c36322aac..31cc96325 100644 --- a/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 +++ b/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 index 30e7c2f8b..18eee2027 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 index c3de64c4c..f639a129e 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 index 6bcc6501b..ed9c9880f 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 index 08479d90e..b098cc49e 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 index 9dc9f98ac..71795cfde 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2 index f3dad679b..adcd5dfa8 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 index 3748eca24..751c5d6bb 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 index 2cabb502e..9e8cd6586 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 index a0e1b62c2..5c2c42202 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 index 2690a0ac9..e9883297e 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 index 871df4827..2c42744ac 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 index 22bd306ee..f24aa6b1b 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 index e57352b8f..dbb653351 100644 --- a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2 b/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2 index 378912490..05bcb762f 100644 --- a/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2 +++ b/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --no-check-models +; COMMAND-LINE: --cegqi-bv --no-check-models ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress1/sygus/Base16_1.sy b/test/regress/regress1/sygus/Base16_1.sy index b84e5bb48..b47060bf8 100644 --- a/test/regress/regress1/sygus/Base16_1.sy +++ b/test/regress/regress1/sygus/Base16_1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all +; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cegqi-full --sygus-out=status --sygus-si=all (set-logic BV) (define-fun B ((h (_ BitVec 8)) (l (_ BitVec 8)) (v (_ BitVec 8))) (_ BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l)))) diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy index 1a7c5888c..b519c570f 100644 --- a/test/regress/regress1/sygus/array_search_2.sy +++ b/test/regress/regress1/sygus/array_search_2.sy @@ -1,6 +1,6 @@ ; REQUIRES: proof ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-si-sol-min-core --proof (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))))) (declare-var x1 Int) diff --git a/test/regress/regress1/sygus/array_search_5-Q-easy.sy b/test/regress/regress1/sygus/array_search_5-Q-easy.sy index dd1783d85..fb1c10337 100644 --- a/test/regress/regress1/sygus/array_search_5-Q-easy.sy +++ b/test/regress/regress1/sygus/array_search_5-Q-easy.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification (set-logic LIA) (synth-fun findIdx ((y1 Int) (y2 Int) (y3 Int) (y4 Int) (y5 Int) (k1 Int)) Int diff --git a/test/regress/regress1/sygus/array_sum_2_5.sy b/test/regress/regress1/sygus/array_sum_2_5.sy index 84046f30a..9490f73b6 100644 --- a/test/regress/regress1/sygus/array_sum_2_5.sy +++ b/test/regress/regress1/sygus/array_sum_2_5.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; 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))))) (declare-var x1 Int) diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy index c9705f7b8..b5d7bff91 100644 --- a/test/regress/regress1/sygus/clock-inc-tuple.sy +++ b/test/regress/regress1/sygus/clock-inc-tuple.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification (set-logic ALL_SUPPORTED) (declare-var m Int) diff --git a/test/regress/regress1/sygus/crcy-si-rcons.sy b/test/regress/regress1/sygus/crcy-si-rcons.sy index 70aec7c4c..177a33274 100644 --- a/test/regress/regress1/sygus/crcy-si-rcons.sy +++ b/test/regress/regress1/sygus/crcy-si-rcons.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status +; 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/regress1/sygus/dt-test-ns.sy b/test/regress/regress1/sygus/dt-test-ns.sy index 90fa57827..f67784002 100644 --- a/test/regress/regress1/sygus/dt-test-ns.sy +++ b/test/regress/regress1/sygus/dt-test-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic DTLIA) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress1/sygus/dup-op.sy b/test/regress/regress1/sygus/dup-op.sy index 517849b2a..dfd99f55d 100644 --- a/test/regress/regress1/sygus/dup-op.sy +++ b/test/regress/regress1/sygus/dup-op.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int) (Con Int)) diff --git a/test/regress/regress1/sygus/enum-test.sy b/test/regress/regress1/sygus/enum-test.sy index 55b2eb69e..b5fbe4306 100644 --- a/test/regress/regress1/sygus/enum-test.sy +++ b/test/regress/regress1/sygus/enum-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) ;; this is the custom enumeration datatype syntax from an early proposal of the sygus standard (define-sort D (Enum (a b))) diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy index 1ae8cabd9..d0027d685 100644 --- a/test/regress/regress1/sygus/error1-dt.sy +++ b/test/regress/regress1/sygus/error1-dt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --sygus-active-gen=enum +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-active-gen=enum (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy index 089a8f11f..ab8852d2e 100644 --- a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy +++ b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic BV) diff --git a/test/regress/regress1/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy index c4c90c6f6..2fdfb1c43 100644 --- a/test/regress/regress1/sygus/hd-sdiv.sy +++ b/test/regress/regress1/sygus/hd-sdiv.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic BV) (define-fun hd01 ((x (_ BitVec 32))) (_ BitVec 32) (bvand x #x00000001)) diff --git a/test/regress/regress1/sygus/int-any-const.sy b/test/regress/regress1/sygus/int-any-const.sy index 18e7ed06e..f377b23c1 100644 --- a/test/regress/regress1/sygus/int-any-const.sy +++ b/test/regress/regress1/sygus/int-any-const.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int) diff --git a/test/regress/regress1/sygus/large-const-simp.sy b/test/regress/regress1/sygus/large-const-simp.sy index d93644197..08f280a4b 100644 --- a/test/regress/regress1/sygus/large-const-simp.sy +++ b/test/regress/regress1/sygus/large-const-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-add-const-grammar +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-add-const-grammar (set-logic LIA) (synth-fun lc ((x Int)) Int) diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy index ae2bcc00e..c6b7d032a 100644 --- a/test/regress/regress1/sygus/list-head-x.sy +++ b/test/regress/regress1/sygus/list-head-x.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic ALL_SUPPORTED) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress1/sygus/max.sy b/test/regress/regress1/sygus/max.sy index f191d784f..e753277cc 100644 --- a/test/regress/regress1/sygus/max.sy +++ b/test/regress/regress1/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress1/sygus/nia-max-square-ns.sy b/test/regress/regress1/sygus/nia-max-square-ns.sy index 5d63ab023..1177be5e7 100644 --- a/test/regress/regress1/sygus/nia-max-square-ns.sy +++ b/test/regress/regress1/sygus/nia-max-square-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --nl-ext-tplanes +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --nl-ext-tplanes (set-logic NIA) (synth-fun max ((x Int) (y Int)) Int) diff --git a/test/regress/regress1/sygus/parity-si-rcons.sy b/test/regress/regress1/sygus/parity-si-rcons.sy index 850cc6610..aea7e32f3 100644 --- a/test/regress/regress1/sygus/parity-si-rcons.sy +++ b/test/regress/regress1/sygus/parity-si-rcons.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi-prereg-inst --sygus-si-rcons=try --sygus-out=status (set-logic BV) diff --git a/test/regress/regress1/sygus/phone-1-long.sy b/test/regress/regress1/sygus/phone-1-long.sy index 0b402acf5..6d89a4e6c 100644 --- a/test/regress/regress1/sygus/phone-1-long.sy +++ b/test/regress/regress1/sygus/phone-1-long.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-fair=direct +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-fair=direct ; EXPECT: unsat (set-logic SLIA) diff --git a/test/regress/regress1/sygus/process-10-vars.sy b/test/regress/regress1/sygus/process-10-vars.sy index 6a9a80a49..86fac86cd 100644 --- a/test/regress/regress1/sygus/process-10-vars.sy +++ b/test/regress/regress1/sygus/process-10-vars.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-arg-relevant +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress1/sygus/qe.sy b/test/regress/regress1/sygus/qe.sy index c8d56229a..eba30350d 100644 --- a/test/regress/regress1/sygus/qe.sy +++ b/test/regress/regress1/sygus/qe.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --sygus-qe-preproc +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-qe-preproc (set-logic LIA) (synth-fun f ((x Int)) Int) diff --git a/test/regress/regress1/sygus/real-any-const.sy b/test/regress/regress1/sygus/real-any-const.sy index 431d0c1b0..53db26910 100644 --- a/test/regress/regress1/sygus/real-any-const.sy +++ b/test/regress/regress1/sygus/real-any-const.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise (set-logic LRA) (synth-fun f ((x Real) (y Real)) Real) diff --git a/test/regress/regress1/sygus/real-grammar.sy b/test/regress/regress1/sygus/real-grammar.sy index 128a94c1d..d664bf2a2 100644 --- a/test/regress/regress1/sygus/real-grammar.sy +++ b/test/regress/regress1/sygus/real-grammar.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none (set-logic LRA) diff --git a/test/regress/regress1/sygus/repair-const-rl.sy b/test/regress/regress1/sygus/repair-const-rl.sy index 6477de3fc..3374d6a8a 100644 --- a/test/regress/regress1/sygus/repair-const-rl.sy +++ b/test/regress/regress1/sygus/repair-const-rl.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-repair-const --lang=sygus2 +; COMMAND-LINE: --sygus-out=status --sygus-si=none --sygus-repair-const --lang=sygus2 (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int diff --git a/test/regress/regress1/sygus/strings-any-term1.sy b/test/regress/regress1/sygus/strings-any-term1.sy index cca2edb2c..2c3eaac33 100644 --- a/test/regress/regress1/sygus/strings-any-term1.sy +++ b/test/regress/regress1/sygus/strings-any-term1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term +; 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) (declare-var x String) diff --git a/test/regress/regress1/sygus/tl-type-0.sy b/test/regress/regress1/sygus/tl-type-0.sy index 0beea8056..3da21f6dc 100644 --- a/test/regress/regress1/sygus/tl-type-0.sy +++ b/test/regress/regress1/sygus/tl-type-0.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int) (Term Int)) diff --git a/test/regress/regress1/sygus/tl-type-4x.sy b/test/regress/regress1/sygus/tl-type-4x.sy index 7c4403397..7d6fa778e 100644 --- a/test/regress/regress1/sygus/tl-type-4x.sy +++ b/test/regress/regress1/sygus/tl-type-4x.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int) (Term Int)) diff --git a/test/regress/regress1/sygus/tl-type.sy b/test/regress/regress1/sygus/tl-type.sy index fe39ddd8e..8be604b23 100644 --- a/test/regress/regress1/sygus/tl-type.sy +++ b/test/regress/regress1/sygus/tl-type.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int) (Term Int)) diff --git a/test/regress/regress1/sygus/twolets1.sy b/test/regress/regress1/sygus/twolets1.sy index b78bf7647..7f3fed923 100644 --- a/test/regress/regress1/sygus/twolets1.sy +++ b/test/regress/regress1/sygus/twolets1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) ;; f1 is x plus 2 ;; f2 is 2x plus 5 diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy index ca1e512a1..16b3e27aa 100644 --- a/test/regress/regress1/sygus/twolets2-orig.sy +++ b/test/regress/regress1/sygus/twolets2-orig.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; 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)) (synth-fun f1 ((x Int)) Int diff --git a/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 b/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 index c26cde173..72743693a 100644 --- a/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 +++ b/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-all --no-check-models +; COMMAND-LINE: --cegqi-all --no-check-models ; EXPECT: sat ;AJR:BROKEN (set-logic UFBV) diff --git a/test/regress/regress2/sygus/lustre-real.sy b/test/regress/regress2/sygus/lustre-real.sy index 99d682bcc..b7637567f 100644 --- a/test/regress/regress2/sygus/lustre-real.sy +++ b/test/regress/regress2/sygus/lustre-real.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIRA) (define-fun __node_init_top_0 ( diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy index fe6f5cd0c..00a0099b0 100644 --- a/test/regress/regress2/sygus/process-10-vars-2fun.sy +++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress2/sygus/process-arg-invariance.sy b/test/regress/regress2/sygus/process-arg-invariance.sy index a50cec2d8..15bffb073 100644 --- a/test/regress/regress2/sygus/process-arg-invariance.sy +++ b/test/regress/regress2/sygus/process-arg-invariance.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress2/sygus/real-grammar-neg.sy b/test/regress/regress2/sygus/real-grammar-neg.sy index 0891e57bf..d9a66bcce 100644 --- a/test/regress/regress2/sygus/real-grammar-neg.sy +++ b/test/regress/regress2/sygus/real-grammar-neg.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --no-sygus-pbe +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --no-sygus-pbe (set-logic LRA) diff --git a/test/regress/regress3/strings-any-term.sy b/test/regress/regress3/strings-any-term.sy index 3827585ec..b84252d6c 100644 --- a/test/regress/regress3/strings-any-term.sy +++ b/test/regress/regress3/strings-any-term.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none (set-logic ALL) (synth-fun f ((x String) (y String)) Int) (declare-var x String) diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index 03fcaab69..74041295d 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -223,7 +223,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); - d_smt->setOption("cbqi-full", CVC4::SExpr(true)); + d_smt->setOption("cegqi-full", CVC4::SExpr(true)); d_smt->setOption("produce-models", CVC4::SExpr(true)); d_scope = new SmtScope(d_smt); -- 2.30.2