summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2020-02-25remove redundant includes (#3815)yoni206
I came across these two redundant includes in theory_uf.h and removed them.
2020-02-24Fixes for quantifiers documentation (#3811)Andrew Reynolds
Minor fixes discovered during development of sygus-inst.
2020-02-24Utilities for words (#3797)Andrew Reynolds
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.
2020-02-24Make lambda rewriter more robust (#3806)Andres Noetzli
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)`.
2020-02-22Minor refactoring of equality notifications (#3798)Andrew Reynolds
Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.
2020-02-22 Move check memberships to reg exp solver (#3793)Andrew Reynolds
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.
2020-02-21Move cardinality inference scheme to base solver in strings (#3792)Andrew Reynolds
Moves handling of cardinality to the base solver, refactors how cardinality is accessed. No intended behavior change in this commit.
2020-02-21Dump boolean propagations and conflicts for decision tree org-mode viewer ↵makaimann
(#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.
2020-02-21Split extended functions solver in strings (#3768)Andrew Reynolds
2020-02-20Remove front-end support for Chain (#3767)Andrew Reynolds
2020-02-20Minor removals (#3786)Andrew Reynolds
Found while working on parser migration of datatypes.
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`). Fixes #3751.
2020-02-19Fix symmetry breaking for multiple sygus types (#3775)Andrew Reynolds
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2020-02-18Fix approximate bounds for transcendental functions whose model values ↵Andrew Reynolds
rewrite (#3747) * Fix bounds for negative sine apps * Format * Comment Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-17Option to limit the number of rounds of enumerative instantiation (#3760)Andrew Reynolds
2020-02-17 Fix soundness bug in reduction of integer div/mod (#3766)Andrew Reynolds
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.
2020-02-16Fix simple issue with cache (#3762)Andrew Reynolds
2020-02-16Activate reverse variant of F-Split inference (#3745)Andres Noetzli
This commit activates the reverse variant of the F-Split inference.
2020-02-15Disable regression (#3761)Andrew Reynolds
Should fix recurring issue with nightlies. Also fixes a warning.
2020-02-15Move proxy variables to InferenceManager in strings (#3758)Andrew Reynolds
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind ↵Andrew Reynolds
arities (#3681)
2020-02-11Fix non-linear equality solving that involves mixed real/integer arithmetic ↵Andrew Reynolds
(#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>
2020-02-11Fix term simplification based on entailment in quantifiers rewriter (#3746)Andrew Reynolds
2020-02-11Remove `--strings-binary-csp` option (#3743)Andres Noetzli
2020-02-10Refactor `CoreSolver::processSimpleNEq()` (#3736)Andres Noetzli
This commit refactors and documents `CoreSolver::processSimpleNEq()`. This method processes equalities between normal forms.
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-07Split strings finite model finding strategy (#3727)Andrew Reynolds
2020-02-07Split core solver from the theory of strings (#3713)Andrew Reynolds
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.
2020-02-07Interface for example evaluation cache utilities (#3726)Andrew Reynolds
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.
2020-02-07Univeset Cardinality constraints for infinite types (#3712)mudathirmahgoub
2020-02-07Statistics for fast enumerator (#3699)Andrew Reynolds
2020-02-07Example evaluation cache utility (#3698)Andrew Reynolds
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-06Generalize containsQuantifiers to hasClosure (#3722)Andrew Reynolds
2020-02-04Articulate proof-related debug statements in arith (#3700)Alex Ozdemir
2020-02-04--fp-exp: Better warning message. (#3709)Aina Niemetz
2020-02-04Split base solver from the theory of strings (#3680)Andrew Reynolds
2020-02-04Revert semantic change from refactoring (#3711)Andres Noetzli
2020-02-03Fix corner case - might need to REWRITE_AGAIN (#3706)Clark Barrett
2020-02-03Fix cardinality of uninterpreted types when univset is not used (#3663)mudathirmahgoub
* 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>
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-02-03Fix corner case of empty domains in bounded fmf (#3690)Andrew Reynolds
2020-02-03Example inference utility (#3670)Andrew Reynolds
2020-01-31Refactor relevance vectors for asserted quantifiers (#3666)Andrew Reynolds
2020-01-31Update sygus grammar normalization to use node-level datatype. (#3567)Andrew Reynolds
2020-01-31Refactor sygus stats (#3684)Andrew Reynolds
2020-01-31Minor refactoring of constructor classes in fast enumerator (#3685)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback