summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2020-02-29 Throw warning instead of error for non-constant values in check-model stages...Andrew Reynolds
2020-02-26More fixes for printing sygus commands (#3812)Andrew Reynolds
2020-02-26Remove portfolio leftovers (#3821)Andres Noetzli
2020-02-24bv_to_int preprocessing passyoni206
2020-02-24Fix bugs related to printing Sygus commands (#3804)Abdalrhman Mohamed
2020-02-20Remove unused code (#3782)Andres Noetzli
2020-02-20Remove parser from bindings (#3779)Andres Noetzli
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2020-02-17Support dumping Sygus commands. (#3763)Abdalrhman Mohamed
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-13Forcing rewrite pass rather than asserting if formula has been rewritten (#3748)Haniel Barbosa
2020-02-12Rename Java package to edu.stanford.CVC4 (#3752)Andres Noetzli
2020-02-08Make "unknown" non-critical for unsat cores check (#3728)Andres Noetzli
2020-02-07Refactor check-model handling in SmtEngine (#3723)Andrew Reynolds
2020-02-06Generalize containsQuantifiers to hasClosure (#3722)Andrew Reynolds
2020-01-31Allow PBE symmetry breaking with sygus stream (#3686)Andrew Reynolds
2020-01-30Weaken assertion for models with approximations (#3667)Andrew Reynolds
2020-01-15New C++ API: Add nullary constructor for Result. (#3603)Aina Niemetz
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-16Support ackermannization on uninterpreted sorts in BV (#3372)Ying Sheng
2019-12-16Trace tags for dumping the decision tree in org-mode format (#2871)makaimann
2019-12-10Allow unsat cores with sygus inference (#3550)Andrew Reynolds
2019-12-09Disable sygus inference when combined with incremental and proofs (#3539)Andrew Reynolds
2019-12-06Throw exception instead of warning for approximate models (#3542)Andrew Reynolds
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-02OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ AP...makaimann
2019-12-01Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)Andrew Reynolds
2019-11-29Check free variables in assertions when using SyGuS (#3504)Andrew Reynolds
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
2019-11-13Distinguish unknown status for model printing (#3454)Andrew Reynolds
2019-11-08cmake: Disable C++ GNU extensions. (#3446)Mathias Preiner
2019-11-04Make check synth solution robust to auxiliary assertions (#3432)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-14Apply sygus repair constant techniques restricted to refinement lemmas (#3386)Andrew Reynolds
2019-10-08pass parameters by reference where it affects performancePiotr Trojanek
2019-10-08Disallow --proof and --incremental (#3332)Andres Noetzli
2019-10-08Make ackermannization generally applicable rather than just BV (#3315)Ying Sheng
2019-10-03Disable proofs for unsupported logics (#3327)yoni206
2019-09-27Make substitution index context-independent (#2474)Andres Noetzli
2019-09-24Return choice functions for approximate values in get-value (#3304)Andrew Reynolds
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-16Return RecoverableModalException when model is not available. (#3283)Andrew Reynolds
2019-09-12Encapsulate synth engine (#3271)Andrew Reynolds
2019-09-06Remove portfolio (#3236)Andrew Reynolds
2019-09-05 Model API for domain elements (#3243)Andrew Reynolds
2019-09-04Towards incremental SyGuS in SMT engine (#3195)Andrew Reynolds
2019-08-28Removing comments related to issues (#3232)Andrew Reynolds
2019-08-27Fixes for get-abduct (#3229)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback