Deletes many unnecessary options, cleans some documentation, consolidates several options.
# other 4 min
trywith 30 --pre-skolem-quant --enum-inst
trywith 30 --inst-when=full --enum-inst
- trywith 30 --no-e-matching --no-quant-cf --enum-inst
+ trywith 30 --no-e-matching --no-cbqi --enum-inst
trywith 30 --enum-inst --quant-ind
- trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --enum-inst
+ trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --enum-inst
trywith 30 --decision=internal --enum-inst --enum-inst-sum
trywith 30 --term-db-mode=relevant --enum-inst
trywith 30 --enum-inst-interleave --enum-inst
trywith 30 --finite-model-find --mbqi=none
trywith 30 --finite-model-find --decision=internal
trywith 30 --finite-model-find --macros-quant --macros-quant-mode=all
- trywith 60 --finite-model-find --fmf-inst-engine
+ trywith 60 --finite-model-find --e-matching
# long runs 4 min
trywith 240 --finite-model-find --decision=internal
finishwith --enum-inst
help = "Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d."
[[option.mode.NO]]
name = "none"
+ help = "Do not add unate lemmas."
[[option]]
name = "arithPropagationMode"
default = "false"
help = "output unsat cores after every UNSAT/VALID response"
-[[option]]
- name = "printUnsatCoresFull"
- category = "regular"
- long = "print-unsat-cores-full"
- type = "bool"
- default = "false"
- help = "dump the full unsat core, including unlabeled assertions"
-
[[option]]
name = "dumpDifficulty"
category = "regular"
type = "bool"
default = "true"
help = "print instantiations for formulas that do not have given identifiers"
+
+[[option]]
+ name = "printUnsatCoresFull"
+ category = "regular"
+ long = "print-unsat-cores-full"
+ type = "bool"
+ default = "false"
+ help = "when printing unsat cores, include unlabeled assertions"
name = "Quantifiers"
# Whether to mini-scope quantifiers.
-# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
-# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
+# Miniscoping is done based on two techniques.
+# First, miniscoping can be done based on conjunctions within quantified
+# formulas. For example, forall x. (P(x) ^ Q(x)) can be rewritten to
+# (forall x. P(x)) ^ (forall x. Q(x))
+# Second, miniscoping can be done based which free variables occur in
+# subformulas of quantified formulas. For example, forall xy. (P(x) V Q(y))
+# can be rewritten to:
+# (forall x. P(x)) V (forall y. Q(y)).
[[option]]
name = "miniscopeQuant"
category = "regular"
- long = "miniscope-quant"
- type = "bool"
- default = "true"
- help = "miniscope quantifiers"
-
-# Whether to mini-scope quantifiers based on formulas with no free variables.
-# For example, forall x. ( P( x ) V Q ) will be rewritten to
-# ( forall x. P( x ) ) V Q
-[[option]]
- name = "miniscopeQuantFreeVar"
- category = "regular"
- long = "miniscope-quant-fv"
- type = "bool"
- default = "true"
- help = "miniscope quantifiers for ground subformulas"
-
-[[option]]
- name = "quantSplit"
- category = "regular"
- long = "quant-split"
- type = "bool"
- default = "true"
- help = "apply splitting to quantified formulas based on variable disjoint disjuncts"
+ long = "miniscope-quant=MODE"
+ type = "MiniscopeQuantMode"
+ default = "CONJ_AND_FV"
+ help = "miniscope mode for quantified formulas"
+ help_mode = "Miniscope quantifiers modes."
+[[option.mode.OFF]]
+ name = "off"
+ help = "Do not miniscope quantifiers."
+[[option.mode.CONJ]]
+ name = "conj"
+ help = "Use miniscoping of conjunctions only."
+[[option.mode.FV]]
+ name = "fv"
+ help = "Use free variable miniscoping only."
+[[option.mode.CONJ_AND_FV]]
+ name = "conj-and-fv"
+ help = "Enable both conjunction and free variable miniscoping."
+[[option.mode.AGG]]
+ name = "agg"
+ help = "Enable aggressive miniscope, which further may rewrite quantified formulas into a form where miniscoping is possible."
[[option]]
name = "prenexQuant"
help_mode = "Prenex quantifiers modes."
[[option.mode.NONE]]
name = "none"
- help = "Do no prenex nested quantifiers."
+ help = "Do not prenex nested quantifiers."
[[option.mode.SIMPLE]]
name = "simple"
help = "Do simple prenexing of same sign quantifiers."
[[option]]
name = "condVarSplitQuant"
category = "regular"
- long = "cond-var-split-quant"
- type = "bool"
- default = "true"
+ long = "cond-var-split-quant=MODE"
+ type = "CondVarSplitQuantMode"
+ default = "ON"
help = "split quantified formulas that lead to variable eliminations"
-
-[[option]]
- name = "condVarSplitQuantAgg"
- category = "regular"
- long = "cond-var-split-agg-quant"
- type = "bool"
- default = "false"
- help = "aggressive split quantified formulas that lead to variable eliminations"
-
+ help_mode = "Modes for splitting quantified formulas that lead to variable eliminations."
+[[option.mode.OFF]]
+ name = "off"
+ help = "Do not split quantified formulas."
+[[option.mode.ON]]
+ name = "on"
+ help = "Split quantified formulas that lead to variable eliminations."
+[[option.mode.AGG]]
+ name = "agg"
+ help = "Aggressively split quantified formulas that lead to variable eliminations."
+
[[option]]
name = "iteDtTesterSplitQuant"
- category = "regular"
+ category = "expert"
long = "ite-dtt-split-quant"
type = "bool"
default = "false"
help = "split ites with dt testers as conditions"
-# Whether to pre-skolemize quantifier bodies.
-# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
-# forall x. P( x ) => f( S( x ) ) = x
[[option]]
name = "preSkolemQuant"
category = "regular"
- long = "pre-skolem-quant"
- type = "bool"
- default = "false"
- help = "apply skolemization eagerly to bodies of quantified formulas"
+ long = "pre-skolem-quant=MODE"
+ type = "PreSkolemQuantMode"
+ default = "OFF"
+ help = "modes to apply skolemization eagerly to bodies of quantified formulas"
+ help_mode = "Modes to apply skolemization eagerly to bodies of quantified formulas."
+[[option.mode.OFF]]
+ name = "off"
+ help = "Do not apply Skolemization eagerly."
+[[option.mode.ON]]
+ name = "on"
+ help = "Apply Skolemization eagerly to top-level (negatively asserted) quantified formulas."
+[[option.mode.AGG]]
+ name = "agg"
+ help = "Apply Skolemization eagerly and aggressively during preprocessing."
+# Whether to pre-skolemize quantifier bodies.
+# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
+# forall x. P( x ) => f( S( x ) ) = x
[[option]]
name = "preSkolemQuantNested"
category = "regular"
default = "true"
help = "apply skolemization to nested quantified formulas"
-[[option]]
- name = "preSkolemQuantAgg"
- category = "regular"
- long = "pre-skolem-quant-agg"
- type = "bool"
- default = "true"
- help = "apply skolemization to quantified formulas aggressively"
-
-[[option]]
- name = "aggressiveMiniscopeQuant"
- category = "regular"
- long = "ag-miniscope-quant"
- type = "bool"
- default = "false"
- help = "perform aggressive miniscoping for quantifiers"
-
[[option]]
name = "elimTautQuant"
category = "regular"
[[option]]
name = "termDbCd"
- category = "regular"
+ category = "expert"
long = "term-db-cd"
type = "bool"
default = "true"
[[option]]
name = "registerQuantBodyTerms"
- category = "regular"
+ category = "expert"
long = "register-quant-body-terms"
type = "bool"
default = "false"
[[option]]
name = "relevantTriggers"
- category = "regular"
+ category = "expert"
long = "relevant-triggers"
type = "bool"
default = "false"
[[option]]
name = "relationalTriggers"
- category = "regular"
+ category = "expert"
long = "relational-triggers"
type = "bool"
default = "false"
[[option]]
name = "purifyTriggers"
- category = "regular"
+ category = "expert"
long = "purify-triggers"
type = "bool"
default = "false"
[[option]]
name = "partialTriggers"
- category = "regular"
+ category = "expert"
long = "partial-triggers"
type = "bool"
default = "false"
[[option]]
name = "consExpandTriggers"
- category = "regular"
+ category = "expert"
long = "cons-exp-triggers"
type = "bool"
default = "false"
[[option]]
name = "multiTriggerWhenSingle"
- category = "regular"
+ category = "expert"
long = "multi-trigger-when-single"
type = "bool"
default = "false"
[[option]]
name = "multiTriggerPriority"
- category = "regular"
+ category = "expert"
long = "multi-trigger-priority"
type = "bool"
default = "false"
[[option]]
name = "multiTriggerCache"
- category = "regular"
+ category = "expert"
long = "multi-trigger-cache"
type = "bool"
default = "false"
[[option]]
name = "multiTriggerLinear"
- category = "regular"
+ category = "expert"
long = "multi-trigger-linear"
type = "bool"
default = "true"
[[option]]
name = "incrementTriggers"
- category = "regular"
+ category = "expert"
long = "increment-triggers"
type = "bool"
default = "true"
[[option]]
name = "instWhenPhase"
- category = "regular"
+ category = "expert"
long = "inst-when-phase=N"
type = "int64_t"
default = "2"
help = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen"
-[[option]]
- name = "instWhenTcFirst"
- category = "regular"
- long = "inst-when-tc-first"
- type = "bool"
- default = "true"
- help = "allow theory combination to happen once initially, before quantifier strategies are run"
-
[[option]]
name = "instMaxLevel"
- category = "regular"
+ category = "expert"
long = "inst-max-level=N"
type = "int64_t"
default = "-1"
help = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)"
-[[option]]
- name = "instLevelInputOnly"
- category = "regular"
- long = "inst-level-input-only"
- type = "bool"
- default = "true"
- help = "only input terms are assigned instantiation level zero"
-
[[option]]
name = "instMaxRounds"
category = "regular"
[[option]]
name = "quantRepMode"
- category = "regular"
+ category = "expert"
long = "quant-rep-mode=MODE"
type = "QuantRepMode"
default = "FIRST"
[[option]]
name = "enumInstRd"
- category = "regular"
+ category = "expert"
long = "enum-inst-rd"
type = "bool"
default = "true"
[[option]]
name = "enumInstLimit"
- category = "regular"
+ category = "expert"
long = "enum-inst-limit=N"
type = "int64_t"
default = "-1"
[[option]]
name = "enumInstStratify"
- category = "regular"
+ category = "expert"
long = "enum-inst-stratify"
type = "bool"
default = "false"
[[option]]
name = "enumInstSum"
- category = "regular"
+ category = "expert"
long = "enum-inst-sum"
type = "bool"
default = "false"
[[option]]
name = "literalMatchMode"
- category = "regular"
+ category = "expert"
long = "literal-matching=MODE"
type = "LiteralMatchMode"
default = "USE"
[[option]]
name = "poolInst"
- category = "regular"
+ category = "expert"
long = "pool-inst"
type = "bool"
default = "true"
[[option]]
name = "quantFunWellDefined"
- category = "regular"
+ category = "expert"
long = "quant-fun-wd"
type = "bool"
default = "false"
[[option]]
name = "mbqiMode"
- category = "regular"
+ category = "expert"
long = "mbqi=MODE"
type = "MbqiMode"
default = "FMC"
[[option]]
name = "fmfOneInstPerRound"
- category = "regular"
+ category = "expert"
long = "mbqi-one-inst-per-round"
type = "bool"
default = "false"
[[option]]
name = "mbqiInterleave"
- category = "regular"
+ category = "expert"
long = "mbqi-interleave"
type = "bool"
default = "false"
help = "interleave model-based quantifier instantiation with other techniques"
-[[option]]
- name = "fmfInstEngine"
- category = "regular"
- long = "fmf-inst-engine"
- type = "bool"
- default = "false"
- help = "use instantiation engine in conjunction with finite model finding"
-
-[[option]]
- name = "fmfFreshDistConst"
- category = "regular"
- long = "fmf-fresh-dc"
- type = "bool"
- default = "false"
- help = "use fresh distinguished representative when applying Inst-Gen techniques"
-
-[[option]]
- name = "fmfFmcSimple"
- category = "regular"
- long = "fmf-fmc-simple"
- type = "bool"
- default = "true"
- help = "simple models in full model check for finite model finding"
-
[[option]]
name = "fmfBoundInt"
category = "regular"
[[option]]
name = "fmfBoundLazy"
- category = "regular"
+ category = "expert"
long = "fmf-bound-lazy"
type = "bool"
default = "false"
[[option]]
name = "fmfTypeCompletionThresh"
- category = "regular"
+ category = "expert"
long = "fmf-type-completion-thresh=N"
type = "int64_t"
default = "1000"
help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
+### Conflict-based instantiation options
+
[[option]]
- name = "quantConflictFind"
+ name = "conflictBasedInst"
category = "regular"
- long = "quant-cf"
+ long = "cbqi"
type = "bool"
default = "true"
- help = "enable conflict find mechanism for quantifiers"
+ help = "enable conflict-based quantifier instantiation"
[[option]]
- name = "qcfMode"
+ name = "cbqiMode"
category = "regular"
- long = "quant-cf-mode=MODE"
+ long = "cbqi-mode=MODE"
type = "QcfMode"
default = "PROP_EQ"
help = "what effort to apply conflict find mechanism"
[[option.mode.PROP_EQ]]
name = "prop-eq"
help = "Apply QCF algorithm to propagate equalities as well as conflicts."
-[[option.mode.PARTIAL]]
- name = "partial"
- help = "Use QCF for conflicts, propagations and heuristic instantiations."
[[option]]
- name = "qcfWhenMode"
- category = "regular"
- long = "quant-cf-when=MODE"
- type = "QcfWhenMode"
- default = "DEFAULT"
- help = "when to invoke conflict find mechanism for quantifiers"
- help_mode = "Quantifier conflict find modes."
-[[option.mode.DEFAULT]]
- name = "default"
- help = "Default, apply conflict finding at full effort."
-[[option.mode.LAST_CALL]]
- name = "last-call"
- help = "Apply conflict finding at last call, after theory combination and and all theories report sat."
-[[option.mode.STD]]
- name = "std"
- help = "Apply conflict finding at standard effort."
-[[option.mode.STD_H]]
- name = "std-h"
- help = "Apply conflict finding at standard effort when heuristic says to."
-
-[[option]]
- name = "qcfTConstraint"
- category = "regular"
- long = "qcf-tconstraint"
+ name = "cbqiTConstraint"
+ category = "expert"
+ long = "cbqi-tconstraint"
type = "bool"
default = "false"
- help = "enable entailment checks for t-constraints in qcf algorithm"
+ help = "enable entailment checks for t-constraints in cbqi algorithm"
[[option]]
- name = "qcfAllConflict"
- category = "regular"
- long = "qcf-all-conflict"
+ name = "cbqiAllConflict"
+ category = "expert"
+ long = "cbqi-all-conflict"
type = "bool"
default = "false"
help = "add all available conflicting instances during conflict-based instantiation"
[[option]]
- name = "qcfNestedConflict"
- category = "regular"
- long = "qcf-nested-conflict"
- type = "bool"
- default = "false"
- help = "consider conflicts for nested quantifiers"
-
-[[option]]
- name = "qcfVoExp"
- category = "regular"
- long = "qcf-vo-exp"
+ name = "cbqiVoExp"
+ category = "expert"
+ long = "cbqi-vo-exp"
type = "bool"
default = "false"
- help = "qcf experimental variable ordering"
+ help = "cbqi experimental variable ordering"
[[option]]
- name = "instNoEntail"
- category = "regular"
- long = "inst-no-entail"
+ name = "cbqiEagerTest"
+ category = "expert"
+ long = "cbqi-eager-test"
type = "bool"
default = "true"
- help = "do not consider instances of quantified formulas that are currently entailed"
+ help = "optimization, test cbqi instances eagerly"
[[option]]
- name = "qcfEagerTest"
- category = "regular"
- long = "qcf-eager-test"
+ name = "cbqiEagerCheckRd"
+ category = "expert"
+ long = "cbqi-eager-check-rd"
type = "bool"
default = "true"
- help = "optimization, test qcf instances eagerly"
+ help = "optimization, eagerly check relevant domain of matched position"
[[option]]
- name = "qcfEagerCheckRd"
- category = "regular"
- long = "qcf-eager-check-rd"
+ name = "cbqiSkipRd"
+ category = "expert"
+ long = "cbqi-skip-rd"
type = "bool"
- default = "true"
- help = "optimization, eagerly check relevant domain of matched position"
+ default = "false"
+ help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
[[option]]
- name = "qcfSkipRd"
+ name = "instNoEntail"
category = "regular"
- long = "qcf-skip-rd"
+ long = "inst-no-entail"
type = "bool"
- default = "false"
- help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
+ default = "true"
+ help = "do not consider instances of quantified formulas that are currently entailed"
### Induction options
[[option]]
name = "quantInduction"
- category = "regular"
+ category = "expert"
long = "quant-ind"
type = "bool"
default = "false"
[[option]]
name = "dtStcInduction"
- category = "regular"
+ category = "expert"
long = "dt-stc-ind"
type = "bool"
default = "false"
[[option]]
name = "intWfInduction"
- category = "regular"
+ category = "expert"
long = "int-wf-ind"
type = "bool"
default = "false"
[[option]]
name = "conjectureGen"
- category = "regular"
+ category = "expert"
long = "conjecture-gen"
type = "bool"
default = "false"
[[option]]
name = "conjectureGenPerRound"
- category = "regular"
+ category = "expert"
long = "conjecture-gen-per-round=N"
type = "int64_t"
default = "1"
[[option]]
name = "conjectureNoFilter"
- category = "regular"
+ category = "expert"
long = "conjecture-no-filter"
type = "bool"
default = "false"
[[option]]
name = "conjectureFilterActiveTerms"
- category = "regular"
+ category = "expert"
long = "conjecture-filter-active-terms"
type = "bool"
default = "true"
[[option]]
name = "conjectureFilterCanonical"
- category = "regular"
+ category = "expert"
long = "conjecture-filter-canonical"
type = "bool"
default = "true"
[[option]]
name = "conjectureFilterModel"
- category = "regular"
+ category = "expert"
long = "conjecture-filter-model"
type = "bool"
default = "true"
[[option]]
name = "conjectureGenGtEnum"
- category = "regular"
+ category = "expert"
long = "conjecture-gen-gt-enum=N"
type = "int64_t"
default = "50"
help = "number of ground terms to generate for model filtering"
-[[option]]
- name = "conjectureUeeIntro"
- category = "regular"
- long = "conjecture-gen-uee-intro"
- type = "bool"
- default = "false"
- help = "more aggressive merging for universal equality engine, introduces terms"
-
[[option]]
name = "conjectureGenMaxDepth"
- category = "regular"
+ category = "expert"
long = "conjecture-gen-max-depth=N"
type = "int64_t"
default = "3"
[[option]]
name = "sygusUnifShuffleCond"
- category = "regular"
+ category = "expert"
long = "sygus-unif-shuffle-cond"
type = "bool"
default = "false"
[[option]]
name = "sygusUnifCondIndNoRepeatSol"
- category = "regular"
+ category = "expert"
long = "sygus-unif-cond-independent-no-repeat-sol"
type = "bool"
default = "true"
[[option]]
name = "sygusBoolIteReturnConst"
- category = "regular"
+ category = "expert"
long = "sygus-bool-ite-return-const"
type = "bool"
default = "true"
[[option]]
name = "sygusQePreproc"
- category = "regular"
+ category = "expert"
long = "sygus-qe-preproc"
type = "bool"
default = "false"
[[option]]
name = "sygusEnumRandomP"
- category = "regular"
+ category = "expert"
long = "sygus-enum-random-p=P"
type = "double"
default = "0.5"
[[option]]
name = "sygusEnumFastNumConsts"
- category = "regular"
+ category = "expert"
long = "sygus-enum-fast-num-consts=N"
type = "uint64_t"
default = "5"
[[option]]
name = "sygusGrammarNorm"
- category = "regular"
+ category = "expert"
long = "sygus-grammar-norm"
type = "bool"
default = "false"
[[option]]
name = "sygusInvAutoUnfold"
- category = "regular"
+ category = "expert"
long = "sygus-auto-unfold"
type = "bool"
default = "true"
[[option]]
name = "sygusPbeMultiFair"
- category = "regular"
+ category = "expert"
long = "sygus-pbe-multi-fair"
type = "bool"
default = "false"
[[option]]
name = "sygusPbeMultiFairDiff"
- category = "regular"
+ category = "expert"
long = "sygus-pbe-multi-fair-diff=N"
type = "int64_t"
default = "0"
[[option]]
name = "sygusEvalUnfoldBool"
- category = "regular"
+ category = "expert"
long = "sygus-eval-unfold-bool"
type = "bool"
default = "true"
[[option]]
name = "cegisSample"
- category = "regular"
+ category = "expert"
long = "cegis-sample=MODE"
type = "CegisSampleMode"
default = "NONE"
name = "trust"
help = "Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures."
-[[option]]
- name = "sygusEvalOpt"
- category = "regular"
- long = "sygus-eval-opt"
- type = "bool"
- default = "true"
- help = "use optimized approach for evaluation in sygus"
-
[[option]]
name = "sygusArgRelevant"
- category = "regular"
+ category = "expert"
long = "sygus-arg-relevant"
type = "bool"
default = "false"
[[option]]
name = "sygusRecFun"
- category = "regular"
+ category = "expert"
long = "sygus-rec-fun"
type = "bool"
default = "true"
[[option]]
name = "sygusRecFunEvalLimit"
- category = "regular"
+ category = "expert"
long = "sygus-rec-fun-eval-limit=N"
type = "uint64_t"
default = "1000"
[[option]]
name = "sygusVerifyInstMaxRounds"
- category = "regular"
+ category = "expert"
long = "sygus-verify-inst-max-rounds=N"
type = "int64_t"
default = "3"
# Internal uses of sygus
-[[option]]
- name = "sygusRew"
- category = "regular"
- long = "sygus-rr"
- type = "bool"
- default = "false"
- help = "use sygus to enumerate and verify correctness of rewrite rules"
-
[[option]]
name = "sygusRewSynth"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth"
type = "bool"
default = "false"
[[option]]
name = "sygusRewSynthFilterOrder"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-filter-order"
type = "bool"
default = "true"
[[option]]
name = "sygusRewSynthFilterMatch"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-filter-match"
type = "bool"
default = "true"
[[option]]
name = "sygusRewSynthFilterCong"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-filter-cong"
type = "bool"
default = "true"
[[option]]
name = "sygusRewSynthFilterNonLinear"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-filter-nl"
type = "bool"
default = "false"
default = "false"
help = "use sygus to verify the correctness of rewrite rules via sampling"
-[[option]]
- name = "sygusRewVerifyAbort"
- category = "regular"
- long = "sygus-rr-verify-abort"
- type = "bool"
- default = "true"
- help = "abort when sygus-rr-verify finds an instance of unsoundness"
-
[[option]]
name = "sygusSamples"
- category = "regular"
+ category = "expert"
long = "sygus-samples=N"
type = "int64_t"
default = "1000"
[[option]]
name = "sygusSampleGrammar"
- category = "regular"
+ category = "expert"
long = "sygus-sample-grammar"
type = "bool"
default = "true"
[[option]]
name = "sygusSampleFpUniform"
- category = "regular"
+ category = "expert"
long = "sygus-sample-fp-uniform"
type = "bool"
default = "false"
[[option]]
name = "sygusRewSynthAccel"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-accel"
type = "bool"
default = "false"
[[option]]
name = "sygusRewSynthCheck"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-check"
type = "bool"
default = "true"
[[option]]
name = "sygusRewSynthInput"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-input"
type = "bool"
default = "false"
[[option]]
name = "sygusRewSynthInputNVars"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-input-nvars=N"
type = "int64_t"
default = "3"
[[option]]
name = "sygusRewSynthInputUseBool"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-input-use-bool"
type = "bool"
default = "false"
[[option]]
name = "sygusRewSynthRec"
- category = "regular"
+ category = "expert"
long = "sygus-rr-synth-rec"
type = "bool"
default = "false"
[[option]]
name = "sygusQueryGenThresh"
- category = "regular"
+ category = "expert"
long = "sygus-query-gen-thresh=N"
type = "uint64_t"
default = "5"
[[option]]
name = "sygusFilterSolMode"
- category = "regular"
+ category = "expert"
long = "sygus-filter-sol=MODE"
type = "SygusFilterSolMode"
default = "NONE"
[[option]]
name = "cegqiFullEffort"
- category = "regular"
+ category = "expert"
long = "cegqi-full"
type = "bool"
default = "false"
[[option]]
name = "cegqiAll"
- category = "regular"
+ category = "expert"
long = "cegqi-all"
type = "bool"
default = "false"
[[option]]
name = "cegqiMultiInst"
- category = "regular"
+ category = "expert"
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 = "cegqiRepeatLit"
- category = "regular"
- long = "cegqi-repeat-lit"
- type = "bool"
- default = "false"
- help = "solve literals more than once in counterexample-based quantifier instantiation"
-
[[option]]
name = "cegqiInnermost"
- category = "regular"
+ category = "expert"
long = "cegqi-innermost"
type = "bool"
default = "true"
[[option]]
name = "cegqiNestedQE"
- category = "regular"
+ category = "expert"
long = "cegqi-nested-qe"
type = "bool"
default = "false"
[[option]]
name = "cegqiUseInfInt"
- category = "regular"
+ category = "expert"
long = "cegqi-use-inf-int"
type = "bool"
default = "false"
[[option]]
name = "cegqiUseInfReal"
- category = "regular"
+ category = "expert"
long = "cegqi-use-inf-real"
type = "bool"
default = "false"
[[option]]
name = "cegqiMinBounds"
- category = "regular"
+ category = "expert"
long = "cegqi-min-bounds"
type = "bool"
default = "false"
[[option]]
name = "cegqiRoundUpLowerLia"
- category = "regular"
+ category = "expert"
long = "cegqi-round-up-lia"
type = "bool"
default = "false"
[[option]]
name = "cegqiMidpoint"
- category = "regular"
+ category = "expert"
long = "cegqi-midpoint"
type = "bool"
default = "false"
[[option]]
name = "cegqiNopt"
- category = "regular"
+ category = "expert"
long = "cegqi-nopt"
type = "bool"
default = "true"
[[option]]
name = "cegqiBvInterleaveValue"
- category = "regular"
+ category = "expert"
long = "cegqi-bv-interleave-value"
type = "bool"
default = "false"
[[option]]
name = "cegqiBvRmExtract"
- category = "regular"
+ category = "expert"
long = "cegqi-bv-rm-extract"
type = "bool"
default = "true"
[[option]]
name = "cegqiBvLinearize"
- category = "regular"
+ category = "expert"
long = "cegqi-bv-linear"
type = "bool"
default = "true"
[[option]]
name = "cegqiBvSolveNl"
- category = "regular"
+ category = "expert"
long = "cegqi-bv-solve-nl"
type = "bool"
default = "false"
[[option]]
name = "cegqiBvConcInv"
- category = "regular"
+ category = "expert"
long = "cegqi-bv-concat-inv"
type = "bool"
default = "true"
[[option]]
name = "hoMatching"
- category = "regular"
+ category = "expert"
long = "ho-matching"
type = "bool"
default = "true"
help = "do higher-order matching algorithm for triggers with variable operators"
-[[option]]
- name = "hoMatchingVarArgPriority"
- category = "regular"
- long = "ho-matching-var-priority"
- type = "bool"
- default = "true"
- help = "give priority to variable arguments over constant arguments"
-
[[option]]
name = "hoMergeTermDb"
- category = "regular"
+ category = "expert"
long = "ho-merge-term-db"
type = "bool"
default = "true"
[[option]]
name = "hoElim"
- category = "regular"
+ category = "expert"
long = "ho-elim"
type = "bool"
default = "false"
[[option]]
name = "hoElimStoreAx"
- category = "regular"
+ category = "expert"
long = "ho-elim-store-ax"
type = "bool"
default = "true"
[[option]]
name = "sygusInstScope"
- category = "regular"
+ category = "expert"
long = "sygus-inst-scope=MODE"
type = "SygusInstScope"
default = "IN"
[[option]]
name = "sygusInstTermSel"
- category = "regular"
+ category = "expert"
long = "sygus-inst-term-sel=MODE"
type = "SygusInstTermSelMode"
default = "MIN"
[[option]]
name = "sygusInstMode"
- category = "regular"
+ category = "expert"
long = "sygus-inst-mode=MODE"
type = "SygusInstMode"
default = "PRIORITY_INST"
[[option]]
name = "setsProxyLemmas"
- category = "regular"
+ category = "expert"
long = "sets-proxy-lemmas"
type = "bool"
default = "false"
[[option]]
name = "setsInferAsLemmas"
- category = "regular"
+ category = "expert"
long = "sets-infer-as-lemmas"
type = "bool"
default = "true"
[[option]]
name = "setsExt"
- category = "regular"
+ category = "expert"
long = "sets-ext"
type = "bool"
default = "false"
default = "false"
help = "produce proofs, support check-proofs and get-proof"
+[[option]]
+ name = "proofMode"
+ category = "expert"
+ long = "proof-mode=MODE"
+ type = "ProofMode"
+ default = "OFF"
+ help = "choose proof mode, see --proof-mode=help"
+ help_mode = "proof modes."
+[[option.mode.OFF]]
+ name = "off"
+[[option.mode.PP_ONLY]]
+ name = "pp-only"
+[[option.mode.SAT]]
+ name = "sat-proof"
+[[option.mode.FULL]]
+ name = "full-proof"
+
[[option]]
name = "checkProofs"
category = "regular"
name = "assumptions"
help = "Produce unsat cores using solving under assumptions and preprocessing proofs."
-[[option]]
- name = "proofMode"
- category = "expert"
- long = "proof-mode=MODE"
- type = "ProofMode"
- default = "OFF"
- help = "choose proof mode, see --proof-mode=help"
- help_mode = "proof modes."
-[[option.mode.OFF]]
- name = "off"
-[[option.mode.PP_ONLY]]
- name = "pp-only"
-[[option.mode.SAT]]
- name = "sat-proof"
-[[option.mode.FULL]]
- name = "full-proof"
-
[[option]]
name = "minimalUnsatCores"
category = "regular"
[[option]]
name = "doITESimp"
- category = "regular"
+ category = "expert"
long = "ite-simp"
type = "bool"
default = "false"
[[option]]
name = "doITESimpOnRepeat"
- category = "regular"
+ category = "expert"
long = "on-repeat-ite-simp"
type = "bool"
default = "false"
[[option]]
name = "extRewPrep"
- category = "regular"
+ category = "expert"
long = "ext-rew-prep=MODE"
type = "ExtRewPrepMode"
default = "OFF"
[[option]]
name = "simplifyWithCareEnabled"
- category = "regular"
+ category = "expert"
long = "simp-with-care"
type = "bool"
default = "false"
[[option]]
name = "compressItes"
- category = "regular"
+ category = "expert"
long = "simp-ite-compress"
type = "bool"
default = "false"
[[option]]
name = "repeatSimp"
- category = "regular"
+ category = "expert"
long = "repeat-simp"
type = "bool"
default = "false"
help = "make multiple passes with nonclausal simplifier"
-[[option]]
- name = "zombieHuntThreshold"
- category = "regular"
- long = "simp-ite-hunt-zombies=N"
- type = "uint64_t"
- default = "524288"
- help = "post ite compression enables zombie removal while the number of nodes is above this threshold"
-
[[option]]
name = "sortInference"
category = "regular"
[[option]]
name = "abstractValues"
- category = "regular"
+ category = "expert"
long = "abstract-values"
type = "bool"
default = "false"
[[option]]
name = "foreignTheoryRewrite"
- category = "regular"
+ category = "expert"
long = "foreign-theory-rewrite"
type = "bool"
default = "false"
long = "strings-infer-sym"
type = "bool"
default = "true"
- help = "strings split on empty string"
+ help = "generalized inferences in strings based on proxy symbols"
[[option]]
name = "stringEagerLen"
name = "abort"
help = "Abort if looping word equations are encountered."
-
[[option]]
name = "stringInferAsLemmas"
category = "regular"
[[option]]
name = "regExpElim"
category = "regular"
- long = "re-elim"
- type = "bool"
- default = "false"
- help = "elimination techniques for regular expressions"
-
-[[option]]
- name = "regExpElimAgg"
- category = "regular"
- long = "re-elim-agg"
- type = "bool"
- default = "false"
- help = "aggressive elimination techniques for regular expressions"
+ long = "re-elim=MODE"
+ type = "RegExpElimMode"
+ default = "OFF"
+ help = "regular expression elimination mode"
+ help_mode = "Regular expression elimination modes."
+[[option.mode.OFF]]
+ name = "off"
+ help = "Do not use regular expression elimination."
+[[option.mode.ON]]
+ name = "on"
+ help = "Use regular expression elimination."
+[[option.mode.AGG]]
+ name = "agg"
+ help = "Use aggressive regular expression elimination."
[[option]]
name = "stringFlatForms"
long = "strings-regexp-inclusion"
type = "bool"
default = "true"
- help = "use regular expression inclusion"
+ help = "use regular expression inclusion for finding conflicts and avoiding regular expression unfolding"
[[option]]
name = "seqArray"
{
// if false, don't bother to reclaim memory here.
NodeManager* nm = NodeManager::currentNM();
- if (nm->poolSize() >= options().smt.zombieHuntThreshold)
+ if (nm->poolSize() >= zombieHuntThreshold)
{
verbose(2) << "..ite simplifier did quite a bit of work.. "
<< nm->poolSize() << endl;
<< " nodes before cleanup" << endl;
d_iteUtilities.clear();
d_env.getRewriter()->clearCaches();
- nm->reclaimZombiesUntil(options().smt.zombieHuntThreshold);
+ nm->reclaimZombiesUntil(zombieHuntThreshold);
verbose(2) << "....node manager contains " << nm->poolSize()
<< " nodes after cleanup" << endl;
}
util::ITEUtilities d_iteUtilities;
Statistics d_statistics;
+
+ static const uint32_t zombieHuntThreshold = 524288;
};
} // namespace passes
//
// We don't want to set this option when we are in logics that contain ALL.
//
- // We also must enable stringExp if reElimAgg is true, since this introduces
- // bounded quantifiers during preprocessing.
+ // We also must enable stringExp if reElim is aggressive, since this
+ // introduces bounded quantifiers during preprocessing.
if ((!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS))
- || opts.strings.regExpElimAgg)
+ || opts.strings.regExpElim == options::RegExpElimMode::AGG)
{
// If the user explicitly set a logic that includes strings, but is not
// the generic "ALL" logic, then enable stringsExp.
opts.smt.sortInference = false;
}
- if (opts.quantifiers.preSkolemQuant)
+ if (opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
{
if (opts.quantifiers.preSkolemQuantWasSetByUser)
{
reason << "pre-skolemization";
return true;
}
- notifyModifyOption("preSkolemQuant", "false", "unsat cores");
- opts.quantifiers.preSkolemQuant = false;
+ notifyModifyOption("preSkolemQuant", "off", "unsat cores");
+ opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::OFF;
}
if (opts.bv.bitvectorToBool)
}
if (!opts.quantifiers.eMatchingWasSetByUser)
{
- opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine;
+ // do not use E-matching by default. For E-matching + FMF, the user should
+ // specify --finite-model-find --e-matching.
+ opts.quantifiers.eMatching = false;
}
if (!opts.quantifiers.instWhenModeWasSetByUser)
{
{
if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
{
- if (!opts.quantifiers.quantConflictFindWasSetByUser)
+ if (!opts.quantifiers.conflictBasedInstWasSetByUser)
{
- opts.quantifiers.quantConflictFind = false;
+ opts.quantifiers.conflictBasedInst = false;
}
if (!opts.quantifiers.instNoEntailWasSetByUser)
{
}
}
// implied options...
- if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint)
+ if (opts.quantifiers.cbqiModeWasSetByUser || opts.quantifiers.cbqiTConstraint)
{
- opts.quantifiers.quantConflictFind = true;
+ opts.quantifiers.conflictBasedInst = true;
}
if (opts.quantifiers.cegqiNestedQE)
{
opts.quantifiers.prenexQuantUser = true;
if (!opts.quantifiers.preSkolemQuantWasSetByUser)
{
- opts.quantifiers.preSkolemQuant = true;
+ opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::ON;
}
}
// for induction techniques
}
}
// can't pre-skolemize nested quantifiers without UF theory
- if (!logic.isTheoryEnabled(THEORY_UF) && opts.quantifiers.preSkolemQuant)
+ if (!logic.isTheoryEnabled(THEORY_UF)
+ && opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
{
if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
{
// optimization: apply preskolemization, makes it succeed more often
if (!opts.quantifiers.preSkolemQuantWasSetByUser)
{
- opts.quantifiers.preSkolemQuant = true;
+ opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::ON;
}
if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
{
{
opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE;
}
- if (!opts.quantifiers.quantConflictFindWasSetByUser)
+ if (!opts.quantifiers.conflictBasedInstWasSetByUser)
{
- opts.quantifiers.quantConflictFind = false;
+ opts.quantifiers.conflictBasedInst = false;
}
if (!opts.quantifiers.instNoEntailWasSetByUser)
{
// should use full effort cbqi for single invocation and repair const
opts.quantifiers.cegqiFullEffort = true;
}
- if (opts.quantifiers.sygusRew)
- {
- opts.quantifiers.sygusRewSynth = true;
- opts.quantifiers.sygusRewVerify = true;
- }
if (opts.quantifiers.sygusRewSynthInput)
{
// If we are using synthesis rewrite rules from input, we use
// do not miniscope
if (!opts.quantifiers.miniscopeQuantWasSetByUser)
{
- opts.quantifiers.miniscopeQuant = false;
- }
- if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser)
- {
- opts.quantifiers.miniscopeQuantFreeVar = false;
- }
- if (!opts.quantifiers.quantSplitWasSetByUser)
- {
- opts.quantifiers.quantSplit = false;
+ opts.quantifiers.miniscopeQuant = options::MiniscopeQuantMode::OFF;
}
// do not do macros
if (!opts.quantifiers.macrosQuantWasSetByUser)
{
Assert(eqt.getType() == tn);
registerPattern(eqt, tn);
- if (isUniversalLessThan(eqt, t)
- || (options().quantifiers.conjectureUeeIntro
- && d_pattern_fun_sum[t] >= d_pattern_fun_sum[eqt]))
+ if (isUniversalLessThan(eqt, t))
{
setUniversalRelevant(eqt);
assertEq = true;
{
arg_to_rep[r] = index;
// function applied to single value, can either use variable or
- // value at this argument position
+ // value at this argument position. We give priority to variables,
+ // although this order could be changed.
d_arg_vector[vnum][index].push_back(bv_at_index);
d_arg_vector[vnum][index].push_back(itf->second);
- if (!options().quantifiers.hoMatchingVarArgPriority)
- {
- std::reverse(d_arg_vector[vnum][index].begin(),
- d_arg_vector[vnum][index].end());
- }
Trace("ho-unif-debug") << " = { self, " << itf->second << " } "
<< std::endl;
}
if( n.hasAttribute(InstLevelAttribute()) ){
return n.getAttribute(InstLevelAttribute());
}
- return options().quantifiers.instLevelInputOnly ? -1 : 0;
+ return -1;
}
else if (options().quantifiers.quantRepMode == options::QuantRepMode::FIRST)
{
}
else
{
- if (options().quantifiers.fmfFreshDistConst)
- {
- mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn);
- }
- else
- {
- // The model basis term cannot be an interpreted function, or else we
- // may produce an inconsistent model by choosing an arbitrary
- // equivalence class for it. Hence, we require that it be an existing or
- // fresh variable.
- mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
- }
+ // The model basis term cannot be an interpreted function, or else we
+ // may produce an inconsistent model by choosing an arbitrary
+ // equivalence class for it. Hence, we require that it be an existing or
+ // fresh variable.
+ mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
}
ModelBasisAttribute mba;
mbt.setAttribute(mba, true);
if( !nv.isConst() ){
Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
}
- Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
+ Node en = hasNonStar ? n
+ : NodeManager::currentNM()->mkNode(APPLY_UF,
+ entry_children);
if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
conds.push_back(n);
return fm->getFunctionValue(op, argPrefix);
}
-
-bool FullModelChecker::useSimpleModels() {
- return options().quantifiers.fmfFmcSimple;
-}
void FullModelChecker::registerQuantifiedFormula(Node q)
{
if (d_quant_cond.find(q) != d_quant_cond.end())
registerNode( qn, true, true );
-
Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
d_mg.reset(new MatchGen(p, this, qn));
is_tsym = true;
d_tsym_vars.push_back( j );
}
- if (!is_tsym || options().quantifiers.qcfTConstraint)
+ if (!is_tsym || options().quantifiers.cbqiTConstraint)
{
d_var_mg[j] = std::make_unique<MatchGen>(p, this, d_vars[j], true);
}
if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
- Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
+ Trace("qcf-invalid")
+ << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
d_mg->setInvalid();
break;
}else{
d_mg->determineVariableOrder(bvars);
}
}else{
- Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
+ Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed."
+ << std::endl;
}
- Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
+ Trace("qcf-qregister-summary")
+ << "QCF register : " << (d_mg->isValid() ? "VALID " : "INVALID") << " : "
+ << q << std::endl;
- if (d_mg->isValid() && options().quantifiers.qcfEagerCheckRd)
+ if (d_mg->isValid() && options().quantifiers.cbqiEagerCheckRd)
{
//optimization : record variable argument positions for terms that must be matched
std::vector< TNode > vars;
//TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
- if (options().quantifiers.qcfSkipRd)
+ if (options().quantifiers.cbqiSkipRd)
{
for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
vars.push_back( d_vars[j] );
{
TNode f = p->getTermDatabase()->getMatchOperator( v );
if( !f.isNull() ){
- Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
+ Trace("qcf-opt") << "Record variable argument positions in " << v
+ << ", op=" << f << "..." << std::endl;
for (size_t k = 0, vnchild = v.getNumChildren(); k < vnchild; k++)
{
Node n = v[k];
std::map<TNode, size_t>::iterator itv = d_var_num.find(n);
if( itv!=d_var_num.end() ){
std::vector<size_t>& vrd = d_var_rel_dom[itv->second][f];
- Trace("qcf-opt") << " arg " << k << " is var #" << itv->second << std::endl;
+ Trace("qcf-opt")
+ << " arg " << k << " is var #" << itv->second << std::endl;
if (std::find(vrd.begin(), vrd.end(), k) == vrd.end())
{
vrd.push_back(k);
Assert(n.getKind() != IMPLIES);
QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
}
- Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
+ Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol
+ << ", rec = " << rec << std::endl;
if( rec ){
for (const Node& nc : n)
{
}
registerNode(n[0], false, pol, beneathQuant);
}
- else if (options().quantifiers.qcfTConstraint)
+ else if (options().quantifiers.cbqiTConstraint)
{
// a theory-specific predicate
for (unsigned i = 0; i < n.getNumChildren(); i++)
bool newHasPol;
bool newPol;
QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- //QcfNode * qcfc = new QcfNode( d_c );
- //qcfc->d_parent = qcf;
- //qcf->d_child[i] = qcfc;
registerNode( n[i], newHasPol, newPol, beneathQuant );
}
}
bool QuantInfo::isTConstraintSpurious(const std::vector<Node>& terms)
{
- if (options().quantifiers.qcfEagerTest)
+ if (options().quantifiers.cbqiEagerTest)
{
EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
//check whether the instantiation evaluates as expected
subs[d_extra_var[i]] = n;
}
if (d_parent->atConflictEffort()) {
- Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
+ Trace("qcf-instance-check")
+ << "Possible conflict instance for " << d_q << " : " << std::endl;
if (!echeck->isEntailed(d_q[1], subs, false, false))
{
- Trace("qcf-instance-check") << "...not entailed to be false." << std::endl;
+ Trace("qcf-instance-check")
+ << "...not entailed to be false." << std::endl;
return true;
}
}else{
// combination of known terms under the current substitution. We use
// the helper method evaluateTerm from the entailment check utility.
Node inst_eval = echeck->evaluateTerm(
- d_q[1], subs, false, options().quantifiers.qcfTConstraint, true);
+ d_q[1], subs, false, options().quantifiers.cbqiTConstraint, true);
if( TraceIsOn("qcf-instance-check") ){
Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
Trace("qcf-instance-check") << " " << terms << std::endl;
- Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
+ Trace("qcf-instance-check")
+ << "...evaluates to " << inst_eval << std::endl;
}
// If it is the case that instantiation can be rewritten to a Boolean
// combination of terms that exist in the current context, then inst_eval
doFail = true;
success = false;
}else{
- if (isBaseMatchComplete() && options().quantifiers.qcfEagerTest)
+ if (isBaseMatchComplete() && options().quantifiers.cbqiEagerTest)
{
return true;
}
if( v==d_vars[index] ){
slv_v = index;
}
- Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
+ Trace("qcf-tconstraint-debug")
+ << "Solve " << d_vars[index] << " = " << v << " "
+ << d_vars[index].getKind() << std::endl;
if (d_vars[index].getKind() == ADD || d_vars[index].getKind() == MULT)
{
Kind k = d_vars[index].getKind();
if( vv==vi ){
//we will assign this
if( slv_v==-1 ){
- Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
+ Trace("qcf-tconstraint-debug")
+ << "...will solve for var #" << vn << std::endl;
slv_v = vn;
if (!d_parent->atConflictEffort())
{
Node z = d_parent->getZero(d_vars[index].getType(), k);
if( !z.isNull() ){
size_t vni = static_cast<size_t>(vn);
- Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
+ Trace("qcf-tconstraint-debug")
+ << "...set " << d_vars[vn] << " = " << z << std::endl;
assigned.push_back(vni);
if (!setMatch(vni, z, false, true))
{
}
}
}else{
- Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;
+ Trace("qcf-tconstraint-debug")
+ << "...sum value " << vv << std::endl;
children.push_back( vv );
}
}else{
}
if( !sum.isNull() ){
assigned.push_back( slv_v );
- Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
+ Trace("qcf-tconstraint-debug")
+ << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
if (!setMatch(slv_v, sum, false, true))
{
success = false;
}
if( !d_unassigned.empty() && ( success || doContinue ) ){
- Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size() << ")..." << std::endl;
+ Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size()
+ << ")..." << std::endl;
do {
if( doFail ){
Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
if( !doFail ){
if( d_una_index<d_unassigned_nvar ){
if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
- Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
+ Trace("qcf-check-unassign")
+ << "Succeeded, variable unconstrained at " << d_una_index
+ << std::endl;
d_una_index++;
}
else if (d_var_mg[d_unassigned[d_una_index]]->getNextMatch())
{
- Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;
+ Trace("qcf-check-unassign") << "Succeeded match with mg at "
+ << d_una_index << std::endl;
d_una_index++;
}
else
{
failed = true;
- Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;
+ Trace("qcf-check-unassign")
+ << "Failed match with mg at " << d_una_index << std::endl;
}
}else{
Assert(doFail || d_una_index + 1 == d_una_eqc_count.size());
d_unassigned[d_una_index], eqcs[currIndex], true, true))
{
d_match_term[d_unassigned[d_una_index]] = TNode::null();
- Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
+ Trace("qcf-check-unassign")
+ << "Succeeded match " << d_una_index << std::endl;
d_una_index++;
}
else
{
- Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;
+ Trace("qcf-check-unassign")
+ << "Failed match " << d_una_index << std::endl;
invalidMatch = true;
}
}
else
{
failed = true;
- Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;
+ Trace("qcf-check-unassign")
+ << "No more matches " << d_una_index << std::endl;
}
}
}
//initialize temporary
d_child_counter = -1;
d_use_children = true;
-
- Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
+
+ Trace("qcf-qregister-debug")
+ << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
std::vector< Node > qni_apps;
d_qni_size = 0;
if( isVar ){
}else if( d_n.getKind()==BOUND_VARIABLE ){
Assert(d_n.getType().isBoolean());
d_type = typ_bool_var;
- }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
+ }
+ else if (d_n.getKind() == EQUAL || options::cbqiTConstraint())
+ {
for (unsigned i = 0; i < d_n.getNumChildren(); i++)
{
if (expr::hasBoundVar(d_n[i]))
Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";
debugPrintType( "qcf-qregister-debug", d_type );
Trace("qcf-qregister-debug") << std::endl;
-
}
void MatchGen::collectBoundVar(Node n,
void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
{
- Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl;
+ Trace("qcf-qregister-debug") << "Determine variable order " << d_n
+ << ", #bvars = " << bvars.size() << std::endl;
bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL );
if( isComm ){
std::map< int, std::vector< int > > c_to_vars;
}
}
//children that bind no unbound variable, then the most number of bound, unbound variables go first
- Trace("qcf-qregister-vo") << "Variable order for " << d_n << " : " << std::endl;
+ Trace("qcf-qregister-vo")
+ << "Variable order for " << d_n << " : " << std::endl;
size_t nqvars = d_qi->d_vars.size();
do {
int min_score0 = -1;
for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
{
if( !assigned[i] ){
- Trace("qcf-qregister-debug2") << "Child " << i << " has b/ub : " << vb_count[i] << "/" << vu_count[i] << std::endl;
+ Trace("qcf-qregister-debug2")
+ << "Child " << i << " has b/ub : " << vb_count[i] << "/"
+ << vu_count[i] << std::endl;
int score0 = 0;//has_nested[i] ? 0 : 1;
int score;
- if( !options::qcfVoExp() ){
+ if (!options::cbqiVoExp())
+ {
score = vu_count[i];
- }else{
+ }
+ else
+ {
score = vu_count[i] == 0 ? 0
: (1 + nqvars * (nqvars - vb_count[i])
+ (nqvars - vu_count[i]));
Trace("qcf-qregister-vo")
<< " " << d_children_order.size() + 1 << ": "
<< d_children[min_score_index]->getNode() << " : ";
- Trace("qcf-qregister-vo") << vu_count[min_score_index] << " " << vb_count[min_score_index] << " " << has_nested[min_score_index] << std::endl;
- Trace("qcf-qregister-debug") << "...assign child " << min_score_index << std::endl;
+ Trace("qcf-qregister-vo")
+ << vu_count[min_score_index] << " " << vb_count[min_score_index]
+ << " " << has_nested[min_score_index] << std::endl;
+ Trace("qcf-qregister-debug")
+ << "...assign child " << min_score_index << std::endl;
Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl;
Assert(min_score_index != -1);
//add to children order
assigned[min_score_index] = true;
//determine order internal to children
d_children[min_score_index]->determineVariableOrder(bvars);
- Trace("qcf-qregister-debug") << "...bind variables" << std::endl;
+ Trace("qcf-qregister-debug") << "...bind variables" << std::endl;
//now, make it a bound variable
if( vu_count[min_score_index]>0 ){
for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
}
}
}
- Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
+ Trace("qcf-qregister-debug")
+ << "...done assign child " << min_score_index << std::endl;
}while( d_children_order.size()!=d_children.size() );
- Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;
+ Trace("qcf-qregister-debug")
+ << "Done assign variable ordering for " << d_n << std::endl;
}else{
for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
{
d_child_counter = 0;
}
}
- else if (d_qi->isBaseMatchComplete() && options::qcfEagerTest())
+ else if (d_qi->isBaseMatchComplete() && options::cbqiEagerTest())
{
d_use_children = false;
d_child_counter = 0;
success = addc!=-1;
//if successful and non-redundant, store that we need to cleanup this
if( addc==1 ){
- //Trace("qcf-explain") << " reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;
for (size_t i = 0; i < 2; i++)
{
if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
if( d_tgt && d_n.getKind()==FORALL ){
//fail
}
- else if (d_n.getKind() == FORALL && d_parent->atConflictEffort()
- && !options::qcfNestedConflict())
+ else if (d_n.getKind() == FORALL && d_parent->atConflictEffort())
{
//fail
}
return !d_qn.empty();
}
-void MatchGen::debugPrintType( const char * c, short typ) {
- switch( typ ){
- case typ_invalid: Trace(c) << "invalid";break;
- case typ_ground: Trace(c) << "ground";break;
- case typ_eq: Trace(c) << "eq";break;
- case typ_pred: Trace(c) << "pred";break;
- case typ_formula: Trace(c) << "formula";break;
- case typ_var: Trace(c) << "var";break;
- case typ_bool_var: Trace(c) << "bool_var";break;
- }
+void MatchGen::debugPrintType(const char* c, short typ)
+{
+ switch (typ)
+ {
+ case typ_invalid: Trace(c) << "invalid"; break;
+ case typ_ground: Trace(c) << "ground"; break;
+ case typ_eq: Trace(c) << "eq"; break;
+ case typ_pred: Trace(c) << "pred"; break;
+ case typ_formula: Trace(c) << "formula"; break;
+ case typ_var: Trace(c) << "var"; break;
+ case typ_bool_var: Trace(c) << "bool_var"; break;
+ }
}
void MatchGen::setInvalid() {
//-------------------------------------------------- check function
bool QuantConflictFind::needsCheck( Theory::Effort level ) {
- bool performCheck = false;
- if (options().quantifiers.quantConflictFind && !d_conflict)
- {
- if( level==Theory::EFFORT_LAST_CALL ){
- performCheck =
- options().quantifiers.qcfWhenMode == options::QcfWhenMode::LAST_CALL;
- }else if( level==Theory::EFFORT_FULL ){
- performCheck =
- options().quantifiers.qcfWhenMode == options::QcfWhenMode::DEFAULT;
- }else if( level==Theory::EFFORT_STANDARD ){
- performCheck =
- options().quantifiers.qcfWhenMode == options::QcfWhenMode::STD;
- }
- }
- return performCheck;
+ return !d_conflict && (level == Theory::EFFORT_FULL);
}
void QuantConflictFind::reset_round( Theory::Effort level ) {
// Returns the beginning of a range of efforts. The value returned is included
// in the range.
inline QuantConflictFind::Effort QcfEffortEnd() {
- return options::qcfMode() == options::QcfMode::PROP_EQ
+ return options::cbqiMode() == options::QcfMode::PROP_EQ
? QuantConflictFind::EFFORT_PROP_EQ
: QuantConflictFind::EFFORT_CONFLICT;
}
/** check */
void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
{
- CodeTimer codeTimer(d_qstate.getStats().d_qcf_time);
+ CodeTimer codeTimer(d_qstate.getStats().d_cbqi_time);
if (quant_e != QEFFORT_CONFLICT)
{
return;
// ensure that quantified formulas that are more likely to have
// conflicting instances are checked earlier.
d_treg.getModel()->markRelevant(q);
- if (options().quantifiers.qcfAllConflict)
+ if (options().quantifiers.cbqiAllConflict)
{
isConflict = true;
}
{
// add quantifiers modules
const Options& options = env.getOptions();
- if (options.quantifiers.quantConflictFind)
+ if (options.quantifiers.conflictBasedInst)
{
d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr));
modules.push_back(d_qcf.get());
d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr));
modules.push_back(d_sg_gen.get());
}
- if (!options.quantifiers.finiteModelFind || options.quantifiers.fmfInstEngine)
+ if (options.quantifiers.eMatching)
{
d_inst_engine.reset(new InstantiationEngine(env, qs, qim, qr, tr));
modules.push_back(d_inst_engine.get());
std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>&
visited) const
{
+ Assert(options().quantifiers.preSkolemQuant
+ != options::PreSkolemQuantMode::OFF);
std::pair<Node, bool> key(n, polarity);
std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>::
iterator it = visited.find(key);
}
else if (polarity)
{
- if (options().quantifiers.preSkolemQuant
- && options().quantifiers.preSkolemQuantNested)
+ if (options().quantifiers.preSkolemQuantNested)
{
std::vector<Node> children;
children.push_back(n[0]);
Assert(n.getType().isBoolean());
if (k == ITE || (k == EQUAL && n[0].getType().isBoolean()))
{
- if (options().quantifiers.preSkolemQuantAgg)
+ if (options().quantifiers.preSkolemQuant
+ == options::PreSkolemQuantMode::AGG)
{
Node nn;
// must remove structure
TrustNode QuantifiersPreprocess::preprocess(Node n, bool isInst) const
{
Node prev = n;
- if (options().quantifiers.preSkolemQuant)
+ if (options().quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
{
if (!isInst || !options().quantifiers.preSkolemQuantNested)
{
return nm->mkNode(AND, conj);
}
}
- if (!d_opts.quantifiers.condVarSplitQuant)
+ if (d_opts.quantifiers.condVarSplitQuant
+ == options::CondVarSplitQuantMode::OFF)
{
return body;
}
// we only do this splitting if miniscoping is enabled, as this is
// required to eliminate variables in conjuncts below. We also never
// miniscope non-standard quantifiers, so this is also guarded here.
- if (!d_opts.quantifiers.miniscopeQuant || !qa.isStandard())
+ if (!doMiniscopeConj(d_opts) || !qa.isStandard())
{
return body;
}
+ bool aggCondSplit = (d_opts.quantifiers.condVarSplitQuant
+ == options::CondVarSplitQuantMode::AGG);
if (bk == ITE
- || (bk == EQUAL && body[0].getType().isBoolean()
- && d_opts.quantifiers.condVarSplitQuantAgg))
+ || (bk == EQUAL && body[0].getType().isBoolean() && aggCondSplit))
{
Assert(!qa.isFunDef());
bool do_split = false;
// Figure out if we should split
// Currently we split if the aggressive option is set, or
// if the top-level OR is binary.
- if (d_opts.quantifiers.condVarSplitQuantAgg || size == 2)
+ if (aggCondSplit || size == 2)
{
do_split = true;
}
}
//computes miniscoping, also eliminates variables that do not occur free in body
-Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa) const
+Node QuantifiersRewriter::computeMiniscoping(Node q,
+ QAttributes& qa,
+ bool miniscopeConj,
+ bool miniscopeFv) const
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> args(q[0].begin(), q[0].end());
}else if( body.getKind()==AND ){
// aggressive miniscoping implies that structural miniscoping should
// be applied first
- if (d_opts.quantifiers.miniscopeQuant
- || d_opts.quantifiers.aggressiveMiniscopeQuant)
+ if (miniscopeConj)
{
BoundVarManager* bvm = nm->getBoundVarManager();
// Break apart the quantifed formula
return retVal;
}
}else if( body.getKind()==OR ){
- if (d_opts.quantifiers.quantSplit)
+ if (miniscopeFv)
{
//splitting subsumes free variable miniscoping, apply it with higher priority
return computeSplit( args, body, qa );
}
- else if (d_opts.quantifiers.miniscopeQuantFreeVar
- || d_opts.quantifiers.aggressiveMiniscopeQuant)
- {
- // aggressive miniscoping implies that free variable miniscoping should
- // be applied first
- Node newBody = body;
- NodeBuilder body_split(kind::OR);
- NodeBuilder tb(kind::OR);
- for (const Node& trm : body)
- {
- if (expr::hasSubterm(trm, args))
- {
- tb << trm;
- }else{
- body_split << trm;
- }
- }
- if( tb.getNumChildren()==0 ){
- return body_split;
- }else if( body_split.getNumChildren()>0 ){
- newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
- std::vector< Node > activeArgs;
- computeArgVec2( args, activeArgs, newBody, qa.d_ipl );
- body_split << mkForAll( activeArgs, newBody, qa );
- return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
- }
- }
}else if( body.getKind()==NOT ){
Assert(isLiteral(body[0]));
}
}
else if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
{
- return d_opts.quantifiers.aggressiveMiniscopeQuant && is_std;
+ return d_opts.quantifiers.miniscopeQuant == options::MiniscopeQuantMode::AGG
+ && is_std;
}
else if (computeOption == COMPUTE_EXT_REWRITE)
{
else if (computeOption == COMPUTE_COND_SPLIT)
{
return (d_opts.quantifiers.iteDtTesterSplitQuant
- || d_opts.quantifiers.condVarSplitQuant)
+ || d_opts.quantifiers.condVarSplitQuant
+ != options::CondVarSplitQuantMode::OFF)
&& !is_strict_trigger;
}
else if (computeOption == COMPUTE_PRENEX)
{
return d_opts.quantifiers.prenexQuant != options::PrenexQuantMode::NONE
- && !d_opts.quantifiers.aggressiveMiniscopeQuant && is_std;
+ && d_opts.quantifiers.miniscopeQuant
+ != options::MiniscopeQuantMode::AGG
+ && is_std;
}
else if (computeOption == COMPUTE_VAR_ELIMINATION)
{
return f;
}
}
+ bool miniscopeConj = doMiniscopeConj(d_opts);
+ bool miniscopeFv = doMiniscopeFv(d_opts);
//return directly
- return computeMiniscoping(f, qa);
+ return computeMiniscoping(f, qa, miniscopeConj, miniscopeFv);
}
std::vector<Node> args(f[0].begin(), f[0].end());
Node n = f[1];
}
}
}
+bool QuantifiersRewriter::doMiniscopeConj(const Options& opts)
+{
+ options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
+ return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
+ || mqm == options::MiniscopeQuantMode::CONJ
+ || mqm == options::MiniscopeQuantMode::AGG;
+}
+
+bool QuantifiersRewriter::doMiniscopeFv(const Options& opts)
+{
+ options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
+ return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
+ || mqm == options::MiniscopeQuantMode::FV
+ || mqm == options::MiniscopeQuantMode::AGG;
+}
bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
if( n.getKind()==FORALL ){
/**
* Compute miniscoping in quantified formula q with attributes in qa.
*/
- Node computeMiniscoping(Node q, QAttributes& qa) const;
+ Node computeMiniscoping(Node q,
+ QAttributes& qa,
+ bool miniscopeConj,
+ bool miniscopeFv) const;
Node computeAggressiveMiniscoping(std::vector<Node>& args, Node body) const;
/**
* This function removes top-level quantifiers from subformulas of body
* q with attributes qa.
*/
bool doOperation(Node q, RewriteStep computeOption, QAttributes& qa) const;
+ /** Whether we should miniscope based on conjunctions based on option */
+ static bool doMiniscopeConj(const Options& opts);
+ /** Whether we should miniscope based on free variables based on option */
+ static bool doMiniscopeFv(const Options& opts);
/**
* Return the rewritten form of q after applying operator computeOption to it.
*/
d_logicInfo(logicInfo)
{
// allow theory combination to go first, once initially
- d_ierCounter = options().quantifiers.instWhenTcFirst ? 0 : 1;
+ d_ierCounter = 0;
d_ierCounterc = d_ierCounter;
d_ierCounterLc = 0;
d_ierCounterLastLc = 0;
QuantifiersStatistics::QuantifiersStatistics()
: d_time(smtStatisticsRegistry().registerTimer(
"theory::QuantifiersEngine::time")),
- d_qcf_time(smtStatisticsRegistry().registerTimer(
- "theory::QuantifiersEngine::time_qcf")),
+ d_cbqi_time(smtStatisticsRegistry().registerTimer(
+ "theory::QuantifiersEngine::time_conflict_based_inst")),
d_ematching_time(smtStatisticsRegistry().registerTimer(
"theory::QuantifiersEngine::time_ematching")),
d_num_quant(smtStatisticsRegistry().registerInt(
public:
QuantifiersStatistics();
TimerStat d_time;
- TimerStat d_qcf_time;
+ TimerStat d_cbqi_time;
TimerStat d_ematching_time;
IntStat d_num_quant;
IntStat d_instantiation_rounds;
options().quantifiers.sygusRepairConstTimeoutWasSetByUser,
options().quantifiers.sygusRepairConstTimeout);
// renable options disabled by sygus
- repcChecker->setOption("miniscope-quant", "true");
- repcChecker->setOption("miniscope-quant-fv", "true");
- repcChecker->setOption("quant-split", "true");
+ repcChecker->setOption("miniscope-quant", "conj-and-fv");
repcChecker->assertFormula(fo_body);
// check satisfiability
Result r = repcChecker->checkSat();
Assert(varlist.size() == args.size());
Node res;
- if (tryEval && options().quantifiers.sygusEvalOpt)
+ if (tryEval)
{
// Try evaluating, which is much faster than substitution+rewriting.
// This may fail if there is a subterm of bn under the
out << ptOut.str();
Assert(bve != bvre);
out << "where they evaluate to " << bve << " and " << bvre << std::endl;
-
- if (options().quantifiers.sygusRewVerifyAbort)
- {
- AlwaysAssert(false)
- << "--sygus-rr-verify detected unsoundness in the rewriter!";
- }
+ AlwaysAssert(false)
+ << "--sygus-rr-verify detected unsoundness in the rewriter!";
}
}
return false;
}
}else{
- if (options().quantifiers.instLevelInputOnly)
- {
- Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
- return false;
- }
+ Trace("inst-add-debug")
+ << "Term " << n << " does not have an instantiation level."
+ << std::endl;
+ return false;
}
}
// it cannot have instantiation constants, which originate from
Trace("quant-engine-proc")
<< "ppNotifyAssertions in QE, #assertions = " << assertions.size()
<< std::endl;
- if (options().quantifiers.instLevelInputOnly
- && options().quantifiers.instMaxLevel != -1)
+ if (options().quantifiers.instMaxLevel != -1)
{
for (const Node& a : assertions)
{
env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_extTheory),
d_rsolver(
env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
- d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()),
+ d_regexp_elim(
+ options().strings.regExpElim == options::RegExpElimMode::AGG,
+ d_pnm,
+ userContext()),
d_stringsFmf(env, valuation, d_termReg),
d_strat(d_env),
d_absModelCounter(0),
}
TrustNode ret;
Node atomRet = atom;
- if (options().strings.regExpElim && atom.getKind() == STRING_IN_REGEXP)
+ if (options().strings.regExpElim != options::RegExpElimMode::OFF
+ && atom.getKind() == STRING_IN_REGEXP)
{
// aggressive elimination of regular expression membership
ret = d_regexp_elim.eliminateTrusted(atomRet);
; EXPECT: sat
(set-logic QF_NRAT)
(set-info :status sat)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
(declare-fun r6 () Real)
(assert (= 0.0 (cos r6)))
(check-sat)
; EXPECT: sat
; EXPECT: sat
(set-logic ALL)
-(set-option :miniscope-quant false)
+(set-option :miniscope-quant off)
(declare-fun i2 () Int)
(declare-fun v6 () Bool)
(declare-sort S2 0)
; EXPECT: sat
(set-logic QF_NRAT)
(set-info :status sat)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
(declare-fun r3 () Real)
(assert (= 0.0 (+ (- r3) (cos r3) (- 1.0))))
(check-sat)
; EXPECT: unsat
; DISABLE-TESTER: unsat-core
(set-logic ALL)
-(set-option :pre-skolem-quant true)
+(set-option :pre-skolem-quant on)
(declare-fun v7 () Bool)
(assert (forall ((q49 Bool) (q55 Bool)) (xor v7 (exists ((q49 Bool)) (xor v7 q49 q49)) v7 (= q55 q49))))
(check-sat)
-; COMMAND-LINE: --re-elim --strings-exp
+; COMMAND-LINE: --re-elim=on --strings-exp
; EXPECT: unsat
(set-logic ALL)
(declare-fun a () String)
(set-logic ALL)
(set-info :status sat)
-(set-option :re-elim-agg true)
-(set-option :re-elim true)
+(set-option :re-elim agg)
(declare-fun str9 () String)
(assert (str.in_re str9 (re.* (re.union re.allchar (str.to_re "lE")))))
(check-sat)
-; COMMAND-LINE: --strings-exp --no-re-elim
+; COMMAND-LINE: --strings-exp
(set-info :status unsat)
(set-logic ALL)
(declare-const actionName String)
-; COMMAND-LINE: --strings-exp --no-re-elim
+; COMMAND-LINE: --strings-exp
(set-info :status sat)
(set-logic QF_SLIA)
(declare-const x String)
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine
+; COMMAND-LINE: --finite-model-find --e-matching
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
+; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone -q
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
+; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone -q
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
; DISABLE-TESTER: unsat-core
; DISABLE-TESTER: proof
(set-logic HO_ALL)
-(set-option :ag-miniscope-quant true)
+(set-option :miniscope-quant agg)
(set-option :conjecture-gen true)
(set-option :int-wf-ind true)
(set-option :sygus-inference true)
(set-logic ALL)
(set-info :status unsat)
-(set-option :ag-miniscope-quant true)
-(set-option :qcf-nested-conflict true)
+(set-option :miniscope-quant agg)
(set-option :macros-quant true)
(set-option :cegqi false)
(set-option :fmf-fun-rlv true)
-; COMMAND-LINE: --qcf-tconstraint
+; COMMAND-LINE: --cbqi-tconstraint
; EXPECT: unsat
(set-logic AUFLIA)
(set-info :source |
-; COMMAND-LINE: --qcf-tconstraint
+; COMMAND-LINE: --cbqi-tconstraint
; EXPECT: unsat
(set-logic AUFLIRA)
(set-info :source |http://proval.lri.fr/why-benchmarks |)
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --sygus-simple-sym-break=none
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=3 --sygus-simple-sym-break=none
; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
; EXIT: 1
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --no-sygus-rr-synth-check
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=1 --sygus-simple-sym-break=none --no-sygus-rr-synth-check
; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
; EXIT: 1
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-simple-sym-break=none
-; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=2 --sygus-simple-sym-break=none
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-synth-check
; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite|\(rewrite)'
; EXIT: 1
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-simple-sym-break=none --fp-exp
; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
; EXIT: 1
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-simple-sym-break=none --fp-exp
; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
; EXIT: 1
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=1 --sygus-simple-sym-break=none
; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
; EXIT: 1
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
(declare-fun e!0 () (Seq Bool))
(assert (= e!0 seq.empty))
(assert (seq.nth e!0 0))
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
; EXPECT: unsat
(set-logic QF_SLIA)
-; COMMAND-LINE: --strings-exp --re-elim
+; COMMAND-LINE: --strings-exp --re-elim=on
; EXPECT: unsat
(set-logic ALL)
(declare-const a String)
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
; EXPECT: unsat
(set-logic ALL)
(declare-fun a () String)
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
; EXPECT: sat
(set-logic ALL)
(declare-fun x () String)
-; COMMAND-LINE: --strings-exp --strings-fmf --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --strings-fmf --re-elim=agg
; EXPECT: sat
(set-logic ALL)
(declare-fun a () String)
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
; EXPECT: sat
(set-logic ALL)
(declare-fun a () String)
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
; EXPECT: sat
(set-logic ALL)
(declare-fun a () String)
; COMMAND-LINE: --strings-exp
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
(set-logic QF_SLIA)
(set-info :status unsat)
(declare-fun a () String)
(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
-(set-option :re-elim true)
+(set-option :re-elim on)
(declare-const actionName String)
(declare-const actionNamespace String)
-; COMMAND-LINE: --strings-exp --re-elim
+; COMMAND-LINE: --strings-exp --re-elim=on
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-logic ALL)
(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
-(set-option :re-elim true)
+(set-option :re-elim on)
(declare-const actionName String)
(declare-const actionNamespace String)
(declare-const example_key String)
(set-info :status sat)
(set-option :produce-models true)
(set-option :strings-exp true)
-(set-option :re-elim true)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
(declare-fun a () String)
(assert (str.in_re a (re.++ (re.+ (str.to_re "AB")) (str.to_re "B"))))
(assert (<= (str.len a) 4))
(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
-(set-option :re-elim false)
+(set-option :re-elim off)
(declare-fun x () String)
(assert (let ((_let_0 (re.* re.allchar ))) (and (not (= (str.in_re x (re.++ _let_0 re.allchar _let_0 (str.to_re (str.++ "A" (str.++ "B" (str.++ "C" "A")))) _let_0 re.allchar _let_0)) (str.in_re x (re.++ _let_0 re.allchar _let_0 re.allchar _let_0 (str.to_re (str.++ "B" (str.++ "C" (str.++ "B" "B")))) _let_0)))) (not (= (str.in_re x (re.++ _let_0 re.allchar _let_0 (str.to_re (str.++ "C" (str.++ "B" "C"))) _let_0 (str.to_re "B") _let_0)) (str.in_re x (re.++ _let_0 re.allchar _let_0 (str.to_re "C") _let_0 (str.to_re (str.++ "B" (str.++ "C" "B"))) _let_0)))))))
(check-sat)
(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
-(set-option :re-elim false)
+(set-option :re-elim off)
(declare-fun x () String)
(assert (let ((_let_0 (re.* re.allchar ))) (and (not (= (str.in_re x (re.++ _let_0 re.allchar _let_0 (str.to_re (str.++ "B" (str.++ "A" (str.++ "C" "B")))) _let_0 re.allchar _let_0)) (str.in_re x (re.++ _let_0 re.allchar _let_0 (str.to_re (str.++ "A" (str.++ "B" (str.++ "C" "C")))) _let_0 re.allchar _let_0)))) (not (= (str.in_re x (re.++ _let_0 re.allchar _let_0 (str.to_re (str.++ "C" (str.++ "B" (str.++ "A" "B")))) _let_0 re.allchar _let_0)) (str.in_re x (re.++ _let_0 re.allchar _let_0 (str.to_re (str.++ "C" (str.++ "B" "A"))) _let_0 (str.to_re "B") _let_0)))))))
(check-sat)
(set-logic QF_SLIA)
(set-info :status unsat)
(set-option :strings-exp true)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
(declare-const x String)
(declare-const y String)
(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
(declare-const x String)
(declare-const y String)
(assert (str.in_re x (re.* (str.to_re "'\r''k'\n'"))))
-; COMMAND-LINE: --no-re-elim
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-logic ALL)
(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
-(set-option :re-elim true)
+(set-option :re-elim on)
(declare-fun x () String)
(assert (str.in_re x (re.++ re.allchar (str.to_re "A") re.allchar (str.to_re "B") re.allchar)))
; EXPECT: sat
; COMMAND-LINE: --sygus-inference
(set-logic ALL)
-(set-option :ag-miniscope-quant true)
+(set-option :miniscope-quant agg)
(set-option :sygus-inference true)
(declare-fun a () Real)
(declare-fun b () Real)
; DISABLE-TESTER: unsat-core
; DISABLE-TESTER: proof
(set-logic ALL)
-(set-option :miniscope-quant true)
+(set-option :miniscope-quant conj-and-fv)
(set-option :sygus-inference true)
(set-option :var-ineq-elim-quant false)
(set-info :status unsat)
(set-logic QF_UFNIA)
(set-info :status sat)
(set-option :cegqi-all true)
-(set-option :quant-split true)
+(set-option :miniscope-quant fv)
(set-option :partial-triggers true)
(set-option :full-saturate-quant true)
(set-option :sygus-inference true)
-; COMMAND-LINE: --strings-exp --re-elim
+; COMMAND-LINE: --strings-exp --re-elim=on
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-option :produce-models true)
-; COMMAND-LINE: --strings-exp --re-elim
+; COMMAND-LINE: --strings-exp --re-elim=on
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
-(set-option :re-elim true)
+(set-option :re-elim on)
(declare-const x String)
(assert (str.in_re x (re.++ (str.to_re "example-bucket/") (re.* re.allchar) (str.to_re "/") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to_re "/foo"))))
(check-sat)
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=3 --no-sygus-sym-break
; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
; EXIT: 1
-; COMMAND-LINE: --strings-exp --no-re-elim
+; COMMAND-LINE: --strings-exp
; EXPECT: unsat
(set-logic QF_SLIA)
(set-info :status unsat)
return (
benchmark_info.benchmark_ext == ".sy"
and "--no-check-synth-sol" not in benchmark_info.command_line_args
- and "--sygus-rr" not in benchmark_info.command_line_args
+ and "--sygus-rr-synth" not in benchmark_info.command_line_args
+ and "--sygus-rr-verify" not in benchmark_info.command_line_args
and "--check-synth-sol" not in benchmark_info.command_line_args
)