summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-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
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-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-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-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
2020-02-07Add `ArithProof::{printInteger,getLfscFunction}` (#3716)Alex Ozdemir
2020-02-07Statistics for fast enumerator (#3699)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback