diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:07 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:21 -0500 |
| commit | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (patch) | |
| tree | 409009a6ab55986308cc73d030db53489beef26d /src/theory/quantifiers/options | |
| parent | 3eaf02c01e74a2a43b2eff7638d6c16171a11a13 (diff) | |
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index a0e42c425..0f9d0f295 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -97,6 +97,8 @@ option fmfFullModelCheck --fmf-fmc bool :default false enable full model check for finite model finding option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding +option fmfFmcCoverSimplify --fmf-fmc-cover-simplify bool :default false + apply covering simplification technique to fmc models option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false only add one instantiation per quantifier per round for fmf |