diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
| commit | a7a9ba359a2a8a26f20ac8fdf5292c4e0e27c76a (patch) | |
| tree | a62e3c29bb702a2e890b234504bbc121c4da2619 /src/theory/quantifiers/options | |
| parent | 7e133dbb7c1adf077102d377d1f7eecae1640ee1 (diff) | |
Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 9e8d02d30..a60f5af78 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -229,16 +229,18 @@ option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::Sygus template mode for sygus invariant synthesis # approach applied to general quantified formulas +option cbqiSplx --cbqi-splx bool :read-write :default false + turns on old implementation of counterexample-based quantifier instantiation option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation -option cbqi2 --cbqi2 bool :read-write :default false - turns on new implementation of counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default true turns on recursive counterexample-based quantifier instantiation option cbqiSat --cbqi-sat bool :read-write :default true answer sat when quantifiers are asserted with counterexample-based quantifier instantiation option cbqiModel --cbqi-model bool :read-write :default true guide instantiations by model values for counterexample-based quantifier instantiation +option cbqiAll --cbqi-all bool :default false + apply counterexample-based instantiation to all quantified formulas option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false use integer infinity for vts in counterexample-based quantifier instantiation option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false |