Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-19 | fixrmBindingsParser | Andres Noetzli | |
2020-02-19 | fix | Andres Noetzli | |
2020-02-19 | Merge branch 'master' into rmBindingsParser | Andres Noetzli | |
2020-02-19 | Remove unused class | 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 | Remove more | Andres Noetzli | |
2020-02-19 | Remove parser from bindings | Andres Noetzli | |
This commit removes the parser from the bindings. Note that it is already in a broken state currently (the reason why CVC4Streams and PipedInput are removed from the Java API examples) and it does not make sense to fix it for the old API. If we want to have some parser facilities with the new API, we should think about a more minimal way of exposing those pieces. This should also fix the bindings issue in #3767 and is work towards #2846. | |||
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 | run_regression: Distinguish between timeout and failure. (#3750) | Mathias Preiner | |
If --use-skip-return-code is enabled and a regression test times out it will return EXIT_SKIP instead of EXIT_FAILURE. | |||
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 | cmake: Remove unused ENABLE_OPTIMIZED option. (#3749) | Mathias Preiner | |
2020-02-11 | Fix term simplification based on entailment in quantifiers rewriter (#3746) | Andrew Reynolds | |
2020-02-11 | Update issue templates | Mathias Preiner | |
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-10 | cmake: Use ld.gold if available for faster link times. (#3738) | Mathias Preiner | |
2020-02-10 | Add more IntReal predicates (#3731) | Alex Ozdemir | |
2020-02-08 | Fix rewrite rules sat regressions (#3734) | Andrew Reynolds | |
Quantifier rewrite rules are not robust to preprocessing within our check-model infrastructure. This disables check-model on 2 satisfiable rewrite rules regressions. Fixes nightlies. | |||
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 | |