diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-02-21 16:16:19 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-21 18:16:19 -0600 |
| commit | a98cd6d50308d1dde1086f0c1502e022bd30ba1b (patch) | |
| tree | 048b40c652c862021b7632343592b3f9e27e2c8b /proofs | |
| parent | 641f14f02de0fb4f6a852fe53eb50b69f34101ee (diff) | |
Switch to th_lira.plf (#3741)
Switches arith_proof.cpp from th_lra to th_lira.
Changes:
Eliminate the d_realMode hack.
instead: modify printOwnedTermAsType prints as integers OR
reals, depending on expectedType.
simultaneously: write printOwnedTermAsType more concisely
also: reimplement printOwnedSort.
Change to the LIRA axioms:
Because they reason about bound types using side conditions, we
no longer need to worry about choosing the correct strictness for
our axiom.
This allows us to cut out a lot of code, rewriting & shrinking
printTheoryLemmaProof.
They also have different names.
This requires us to change a lot of string literals
enable proof-checking for many tests.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/signatures/CMakeLists.txt | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt index 86474585c..698fa37fe 100644 --- a/proofs/signatures/CMakeLists.txt +++ b/proofs/signatures/CMakeLists.txt @@ -16,7 +16,7 @@ set(core_signature_files th_bv_rewrites.plf th_real.plf th_int.plf - th_lra.plf + th_lira.plf ) set(CORE_SIGNATURES "") |