diff options
| author | Martin <martin.brain@cs.ox.ac.uk> | 2017-10-10 07:21:26 +0100 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-09 23:21:26 -0700 |
| commit | 8c860213ca3a43e1fe483accb4b2b928ae14028e (patch) | |
| tree | 4383636a3c88e1cde14e78b9ee4f04f46952c392 /src/Makefile.am | |
| parent | 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 (diff) | |
Add skeleton of the FP theory solver (#1130)
This commit adds the skeleton of the theory solver using a dummy version of the converter (fp_converter.{h,cpp}). The converter is a class that is used to produce bit-vector expressions equivalent to floating-point ones. The commit sets up the equality engine and the infrastructure for interacting with the main theory components. The majority of this code is still agnostic to how the conversion is actually implemented / what kind of theory solver this is. This is pretty much the template code you need to write any kind of theory solver. This includes equality reasoning and so should be able to solve some basic problems.
Diffstat (limited to 'src/Makefile.am')
| -rw-r--r-- | src/Makefile.am | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 9412e3433..76d95ea4b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -330,6 +330,8 @@ libcvc4_la_SOURCES = \ theory/fp/theory_fp_rewriter.h \ theory/fp/theory_fp_type_rules.h \ theory/fp/type_enumerator.h \ + theory/fp/fp_converter.h \ + theory/fp/fp_converter.cpp \ theory/idl/idl_assertion.cpp \ theory/idl/idl_assertion.h \ theory/idl/idl_assertion_db.cpp \ |