summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-26Support for witnessing choice in models (#3781)Andrew Reynolds
Fixes #3300. This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
2020-02-26Remove portfolio leftovers (#3821)Andres Noetzli
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio build but there were some leftovers. This commit removes them.
2020-02-26Minor cleaning of smt2 parser (#3823)Andrew Reynolds
Towards parser migration, will make the diff of the eventual conversion a bit smaller.
2020-02-25Embed mkAssociative utilities within the API. (#3801)Andrew Reynolds
Towards parser/API migration.
2020-02-25Sets & Relations Java example (#3816)mudathirmahgoub
Fixes [(Bugzilla #677)](https://github.com/CVC4/cvc4-projects/issues/25).
2020-02-25Sets & Relations Java example (#3816)mudathirmahgoub
2020-02-25remove redundant includes (#3815)yoni206
I came across these two redundant includes in theory_uf.h and removed them.
2020-02-24bv_to_int preprocessing passyoni206
Introduces a preprocessing pass that translates bv problems to integer problems.
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-24Convert parser input interface to api::Term (#3809)Andrew Reynolds
2020-02-24Fix bugs related to printing Sygus commands (#3804)Abdalrhman Mohamed
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.
2020-02-24Add missing functions to new C++ API (#3769)Andrew Reynolds
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-22RIP th_lra.plf (#3796)Alex Ozdemir
Rest in Peace, old LRA signature.
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-21Switch to th_lira.plf (#3741)Alex Ozdemir
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.
2020-02-21New C++ API: Remove TOTAL kinds. (#3794)Aina Niemetz
2020-02-21Simple changes towards unicode string standard (#3791)Andrew Reynolds
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.
2020-02-21Adding checks to the validation of 'bv-sat-solver' to ensure that the ↵Andrew V. Jones
selected SAT solver is compiled-in (#3771)
2020-02-21Split extended functions solver in strings (#3768)Andrew Reynolds
2020-02-21Remove IntReal tightening axioms from th_lira.plf (#3787)Alex Ozdemir
2020-02-20Remove front-end support for Chain (#3767)Andrew Reynolds
2020-02-20Remove unused code (#3782)Andres Noetzli
2020-02-20Minor removals (#3786)Andrew Reynolds
Found while working on parser migration of datatypes.
2020-02-20Remove parser from bindings (#3779)Andres Noetzli
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-19Add Python bindings using Cython -- see below for more details (#2879)makaimann
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2020-02-19Change Record to shared_ptr (#3778)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-18Change datatype selector/constructor/tester to terms (#3773)makaimann
2020-02-18Add missing kinds for the new API (#3757)Andrew Reynolds
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-17Using ParseOp in TPTP (#3764)Haniel Barbosa
2020-02-17Support dumping Sygus commands. (#3763)Abdalrhman Mohamed
2020-02-16Fix simple issue with cache (#3762)Andrew Reynolds
2020-02-16Add temporary global API conversion utilities. (#3759)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-13Update sygus v1 parser to use ParseOp utility (#3756)Andrew Reynolds
2020-02-13Forcing rewrite pass rather than asserting if formula has been rewritten (#3748)Haniel Barbosa
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.
2020-02-13Const input for sygus print callback (#3755)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback