summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-19fixrmBindingsParserAndres Noetzli
2020-02-19fixAndres Noetzli
2020-02-19Merge branch 'master' into rmBindingsParserAndres Noetzli
2020-02-19Remove unused classAndres 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-19Remove moreAndres Noetzli
2020-02-19Remove parser from bindingsAndres 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-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
2020-02-12[Python] Properly destroy CVC4 object (#3753)Andres Noetzli
2020-02-12Rename Java package to edu.stanford.CVC4 (#3752)Andres Noetzli
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind ↵Andrew Reynolds
arities (#3681)
2020-02-11run_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-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-11cmake: Remove unused ENABLE_OPTIMIZED option. (#3749)Mathias Preiner
2020-02-11Fix term simplification based on entailment in quantifiers rewriter (#3746)Andrew Reynolds
2020-02-11Update issue templatesMathias Preiner
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-10Implement LFSCArithProof::equalityType. (#3740)Alex Ozdemir
Also, missed an armType use.
2020-02-10Add 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-10cmake: Use ld.gold if available for faster link times. (#3738)Mathias Preiner
2020-02-10Add more IntReal predicates (#3731)Alex Ozdemir
2020-02-08Fix 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-08Make "unknown" non-critical for unsat cores check (#3728)Andres Noetzli
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-07Refactor check-model handling in SmtEngine (#3723)Andrew Reynolds
2020-02-07Propagate expected types through UF arguments (#3717)Alex Ozdemir
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback