Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-21 | Dump 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-21 | Switch 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-21 | New C++ API: Remove TOTAL kinds. (#3794) | Aina Niemetz | |
2020-02-21 | Simple 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-21 | Adding checks to the validation of 'bv-sat-solver' to ensure that the ↵ | Andrew V. Jones | |
selected SAT solver is compiled-in (#3771) | |||
2020-02-21 | Split extended functions solver in strings (#3768) | Andrew Reynolds | |
2020-02-20 | Remove front-end support for Chain (#3767) | Andrew Reynolds | |
2020-02-20 | Remove unused code (#3782) | Andres Noetzli | |
2020-02-20 | Minor removals (#3786) | Andrew Reynolds | |
Found while working on parser migration of datatypes. | |||
2020-02-20 | Remove parser from bindings (#3779) | Andres Noetzli | |
2020-02-19 | resource 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-19 | Fix symmetry breaking for multiple sygus types (#3775) | Andrew Reynolds | |
2020-02-19 | Add Python bindings using Cython -- see below for more details (#2879) | makaimann | |
2020-02-19 | Delay enumerative instantiation if theory engine does not need check (#3774) | Andrew Reynolds | |
2020-02-19 | Change Record to shared_ptr (#3778) | Andrew Reynolds | |
2020-02-18 | Fix 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-18 | Change datatype selector/constructor/tester to terms (#3773) | makaimann | |
2020-02-18 | Add missing kinds for the new API (#3757) | Andrew Reynolds | |
2020-02-17 | Option 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-17 | Using ParseOp in TPTP (#3764) | Haniel Barbosa | |
2020-02-17 | Support dumping Sygus commands. (#3763) | Abdalrhman Mohamed | |
2020-02-16 | Fix simple issue with cache (#3762) | Andrew Reynolds | |
2020-02-16 | Add temporary global API conversion utilities. (#3759) | Andrew Reynolds | |
2020-02-16 | Activate reverse variant of F-Split inference (#3745) | Andres Noetzli | |
This commit activates the reverse variant of the F-Split inference. | |||
2020-02-15 | Disable regression (#3761) | Andrew Reynolds | |
Should fix recurring issue with nightlies. Also fixes a warning. | |||
2020-02-15 | Move proxy variables to InferenceManager in strings (#3758) | Andrew Reynolds | |
2020-02-14 | Remove quantifiers rewrite rules infrastructure (#3754) | Andrew Reynolds | |
2020-02-13 | Update sygus v1 parser to use ParseOp utility (#3756) | Andrew Reynolds | |
2020-02-13 | Forcing 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-13 | Const input for sygus print callback (#3755) | Andrew Reynolds | |
2020-02-12 | [Python] Properly destroy CVC4 object (#3753) | Andres Noetzli | |
2020-02-12 | Rename Java package to edu.stanford.CVC4 (#3752) | Andres Noetzli | |
2020-02-12 | Ensure ext rewrites for associative ops dont throw assertions for kind ↵ | Andrew Reynolds | |
arities (#3681) | |||
2020-02-11 | Fix 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-11 | Fix term simplification based on entailment in quantifiers rewriter (#3746) | Andrew Reynolds | |
2020-02-11 | Remove `--strings-binary-csp` option (#3743) | Andres Noetzli | |
2020-02-10 | Refactor `CoreSolver::processSimpleNEq()` (#3736) | Andres Noetzli | |
This commit refactors and documents `CoreSolver::processSimpleNEq()`. This method processes equalities between normal forms. | |||
2020-02-10 | Use example evaluation cache instead of sygus PBE (#3733) | Andrew Reynolds | |
2020-02-10 | Implement LFSCArithProof::equalityType. (#3740) | Alex Ozdemir | |
Also, missed an armType use. | |||
2020-02-10 | Add function for tightening literals (#3732) | Alex Ozdemir | |
* Add function for tightening literals The function tightens a literal if it can be tightened, and prints a proof of the result. * Include a #include Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> | |||
2020-02-08 | Make "unknown" non-critical for unsat cores check (#3728) | Andres Noetzli | |
2020-02-07 | Split strings finite model finding strategy (#3727) | Andrew Reynolds | |
2020-02-07 | Split 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-07 | Interface 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-07 | Univeset Cardinality constraints for infinite types (#3712) | mudathirmahgoub | |
2020-02-07 | Refactor check-model handling in SmtEngine (#3723) | Andrew Reynolds | |
2020-02-07 | Propagate expected types through UF arguments (#3717) | Alex Ozdemir | |
2020-02-07 | Add `ArithProof::{printInteger,getLfscFunction}` (#3716) | Alex Ozdemir | |
2020-02-07 | Statistics for fast enumerator (#3699) | Andrew Reynolds | |