Age | Commit message (Collapse) | Author |
|
In PR #3398, a minor change was introduced: One of the checks for
whether there is a conflict or not was flipped
(https://github.com/CVC4/CVC4/pull/3398/files#diff-62fffb0d9df0385909621e424bdcef72R1652). This commit reverts that change.
|
|
* Add more arith proof regression tests
These tests are designed to test interesting cases of arithmetic proofs,
such as mixing integers and reals and tightening bounds.
Right now, they have the --no-check-proofs flag set, which prevents them
from testing the proof machinery. However, once we check that machinery
into master, we'll remove that flag, thus enabling the full effect of
the tests.
* A few comments explaining things.
* Add another tightening test
* Add new test to CMake
* No --no-check-models. There are no models anyway.
* Delete smt-lib-version, per Yoni
|
|
Fixes #3565.
|
|
|
|
|
|
Fixes two issues in regressions, fixes regress1.
|
|
* Fixed bug 3662
* format
* small change
* added bug3663.smt2 file
* throw Logic Exception
* throw Logic Exception
* ;EXIT: 1
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
|
|
|
|
|
|
|
|
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
`TheoryProofEngine` now uses the `expectedType` optional argument.
* When printing terms, it sets this for theories that it dispatches too
* It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
* It is mindful of `expectedType` when using the let map.
I also moved to hpp function implementations into the cpp.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We don't run check-model for models with approximate values, however we were still running the internal debugCheckModel method, which leads to assertion failures. This disables this check.
Fixes #3652.
|
|
|
|
|
|
|
|
* expectedType in proof-printing code
To print lemma proofs in theories that use multiple sorts that have a
subtype relationship, we need to increase communication between the
TheoryProofEngine and the theory proofs themselves.
This commit add an (optional) argument `expectedType` to many
term-printing functions in TheoryProofEngine and TheoryProof.
Right now it is unused, so always takes on the default value of "null"
(meaning no type expectation), but in the future the TheoryProofEngine
will use it to signal TheoryProof about what type is expected to be
printed.
* TypeNode, Don't mix default args & virtual
* Use TypeNode instead of Type (The former are lighter)
* Don't add default arguments to virtual functions, because these cannot
be dynamically overriden during a dynamic dispatch.
* Since we don't want them to be overidable anyway, we use two
functions: one that is non-virtual and has a default, the other that
is virtual but has no default. The former just calls the latter.
* clang-format after signature changes
|
|
|
|
|
|
|
|
* Axioms for affine function bounds. Tests.
* Apply suggestions from code review
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Clarify descriptions of th_lira tests
Thanks, Yoni!
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
|
|
|
|
(#3641)
|
|
* Fix for 3614
* Add regression
* Remove regression
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
|
|
|
|
|
|
|
|
* Types and side conditions for affine bounds
Bounds (being positive, non-negative) actually have an arithmetic.
This PR defines that.
Useful b/c Farkas proofs are basically just sums of bounded affine
functions.
* Address Yoni's comments. Thanks!
* Moved a positivity-test to th_real
* Describe what an affine bound is in better detail
|
|
Used for proving that real terms are affine functions of their
variables.
|
|
This commit introduces types for linear combinations of arith variables
along with side conditions for their arithmetic.
It does the same for affine functions.
These primitives are ultimately used in our machinery for Farkas proofs.
|
|
* Axioms (and side conditions) for tightening bounds
* Side conditions for verifying floor/ceiling-like functions
* Axioms for their correct execution
* Axioms for bound tightening.
* Apply suggestions from code review
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Address Yoni's comments by addings documentation.
Thanks Yoni!
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
|
|
* Merge branch 'master' into lira-pf-arith-pred
* Shorten reify_arith_pred, thanks Yoni!
Use recursion!
* typo
|
|
* LIRA sig: int, real terms, and conversions
* Address Yoni's comments.
* Better description of "reify" functions
* explicit (rather than implicit) `fail` when reifying integer division
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
|
|
|