Age | Commit message (Collapse) | Author |
|
Fixes [(Bugzilla #677)](https://github.com/CVC4/cvc4-projects/issues/25).
|
|
|
|
I came across these two redundant includes in theory_uf.h and removed them.
|
|
Introduces a preprocessing pass that translates bv problems to integer problems.
|
|
Minor fixes discovered during development of sygus-inst.
|
|
This adds a utility file for handling operations over constant "words" (this will eventually generalize string or sequence constants). This is work towards CVC4/cvc4-projects#23.
Also improves documentation in regexp.h.
|
|
|
|
With this commit, most Sygus problems should print correctly. The current printing functionality was tested on 158 Sygus regress files (0, 1, and 2) and 153 of them were printed in Sygus2 format and contained "(check-synth)". The printing functionality was tested again on the generated files and gave almost the same results.
|
|
|
|
The lambda rewriter was not robust to the case where the lambda of the
array representation contained a disequality, e.g. `not(x = 1))`. It
would process it as `ite(not(x = 1), true, false)` instead of `ite(x =
1, false, true)`, which meant that it wasn't able to turn it into an
array representation when checking const-ness. Additionally, the
rewriter had issues when the lambda was of the form `ite((= x c1), true,
(= y c2))` (after turning it into an array and then into a lambda)
because it is expecting the false branch of the `ite` to not contain `y`
variables, making it non-constant despite the array being constant. This
commit solves that issue by normalizing `ite(not(c), x, y) ---> ite(c,
y, x)`.
|
|
Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.
|
|
Rest in Peace, old LRA signature.
|
|
There was previously a function in TheoryStrings to make the proper call to checkMembership. In the refactored code, this is no longer necessary and the interface to RegExp can be simplified.
|
|
Moves handling of cardinality to the base solver, refactors how cardinality is accessed.
No intended behavior change in this commit.
|
|
(#3788)
PR #2871 added trace tags for dumping the decision tree in org-mode format. However, it only dumped theory propagations/conflicts. This could be confusing because it would appear to backtrack without reaching a conflict (but actually the conflict was at the propositional level). This commit also adds dumping of boolean propagations and conflicts.
|
|
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.
|
|
|
|
This updates --lang=smt2.6.1 with the minor syntactic differences from the current syntax and the standard here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.
The next steps will be to address the more invasive changes required to support the standard.
|
|
selected SAT solver is compiled-in (#3771)
|
|
|
|
|
|
|
|
|
|
Found while working on parser migration of datatypes.
|
|
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
|
|
|
|
|
|
|
|
rewrite (#3747)
* Fix bounds for negative sine apps
* Format
* Comment
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
|
|
|
|
|
|
|
|
This was introduced 7 years ago in https://github.com/CVC4/CVC4/commit/9098391fe334d829ec4101f190b8f1fa21c30752.
This impacted any case of integer div/mod of the form `(mod c t)` or `(div c t)` where c is a constant and `t` is not.
Fixes #3765.
Also improves `--dump=t-lemmas` trace to result in smt-lib compatible output, which was required for debugging this.
|
|
|
|
|
|
|
|
|
|
This commit activates the reverse variant of the F-Split inference.
|
|
Should fix recurring issue with nightlies.
Also fixes a warning.
|
|
|
|
|
|
|
|
This ensures that users or developers don't accidentally break the solver either via options or changing the SMT engine flow so that the formula is not rewritten up to a given point.
|
|
|
|
|
|
|
|
arities (#3681)
|
|
If --use-skip-return-code is enabled and a regression test times out it
will return EXIT_SKIP instead of EXIT_FAILURE.
|