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/Makefile.am | |
| 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/Makefile.am')
| -rw-r--r-- | src/Makefile.am | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 90a4d6f5b..95ca44e63 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -337,9 +337,11 @@ libcvc4_la_SOURCES = \ theory/quantifiers/fun_def_process.h \ theory/quantifiers/fun_def_process.cpp \ theory/quantifiers/fun_def_engine.h \ - theory/quantifiers/fun_def_engine.cpp \ - theory/quantifiers/quant_equality_engine.h \ - theory/quantifiers/quant_equality_engine.cpp \ + theory/quantifiers/fun_def_engine.cpp \ + theory/quantifiers/quant_equality_engine.h \ + theory/quantifiers/quant_equality_engine.cpp \ + theory/quantifiers/ceg_instantiator.h \ + theory/quantifiers/ceg_instantiator.cpp \ theory/quantifiers/options_handlers.h \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ |