summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-02-21Dump boolean propagations and conflicts for decision tree org-mode viewer (#3...makaimann
2020-02-21Switch to th_lira.plf (#3741)Alex Ozdemir
2020-02-21New C++ API: Remove TOTAL kinds. (#3794)Aina Niemetz
2020-02-21Simple changes towards unicode string standard (#3791)Andrew Reynolds
2020-02-21Adding checks to the validation of 'bv-sat-solver' to ensure that the selecte...Andrew V. Jones
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
2020-02-20Remove parser from bindings (#3779)Andres Noetzli
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
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 rewrit...Andrew Reynolds
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
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
2020-02-15Disable regression (#3761)Andrew Reynolds
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
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 aritie...Andrew Reynolds
2020-02-11Fix non-linear equality solving that involves mixed real/integer arithmetic (...Andrew Reynolds
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
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-10Implement LFSCArithProof::equalityType. (#3740)Alex Ozdemir
2020-02-10Add function for tightening literals (#3732)Alex Ozdemir
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
2020-02-07Interface for example evaluation cache utilities (#3726)Andrew Reynolds
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