Age | Commit message (Collapse) | Author |
|
I came across these two redundant includes in theory_uf.h and removed them.
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
arities (#3681)
|
|
(#3739)
* Fix non-linear equality solving that involves mixed real/integer.
* Format
* Fix
* Revert
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
|
|
|
|
|
|
This commit refactors and documents `CoreSolver::processSimpleNEq()`.
This method processes equalities between normal forms.
|
|
|
|
|
|
This splits the main procedure from Liang et al CAV 2014 to its own file, the "core solver" of theory of strings.
I have intentionally not updated or clang-formatted the code in core_solver.cpp since I would prefer this PR to involve as little change to behavior as possible (it is copied verbatim from theory_strings.cpp). Future PRs will clean this code up.
|
|
This adds interfaces in synth_conjecture for getting an ExampleEvalCache, per enumerator.
It also adds a specialization `checkRefinementEvalLemmas` of `getRefinementEvalLemmas` in the cegis module, which does evaluation on CEGIS refinement lemmas without structural generalization. This function will be used as an alternative to `getRefinementEvalLemmas` for fast enumerators.
The next PR will update all utilities to use ExampleEvalCache instead of SygusPbe for evaluating examples.
|
|
|
|
|
|
|
|
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* 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>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|