summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2017-12-10Add new infrastructure for preprocessing passes (#1053)justinxu421
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
2017-11-29Minor improvements and changes to defaults for cbqi bv (#1406)Andrew Reynolds
2017-11-29Improve caching in term formula removal (#1398)Andrew Reynolds
2017-11-27Fix models for --solve-real-as-int. (#1371)Andrew Reynolds
2017-11-17(Refactor) Document and clean single invocation partition. (#1364)Andrew Reynolds
2017-11-17Add random number generator. (#1370)Aina Niemetz
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-14Cleaning up exporting vectors within commands. Resolves CID 1172285 and 11722...Tim King
2017-11-13Disable sygus qe preprocessing by default (#1353)Andrew Reynolds
2017-11-09Higher-order prep (#1338)Andrew Reynolds
2017-11-07Allow FORALL in quantifier elimination command (#1322)Andrew Reynolds
2017-11-03Sygus clean main (#1297)Andrew Reynolds
2017-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
2017-10-28Change bvudiv semantics based on input language (#1292)Andres Noetzli
2017-10-27Implement Hilbert choice operator (#1291)Andrew Reynolds
2017-10-26Adds a macro to SWIG to ignore the override and final C++11 keywords in older...Tim King
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
2017-10-17Making the values argument const in the SetUserAttributeCommand const… (#1249)Tim King
2017-10-16Fix for issue 1247 (#1257)Clark Barrett
2017-10-11Ho Lambda Lifting (#1116)Andrew Reynolds
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
2017-10-09Split term database (#1206)Andrew Reynolds
2017-09-26Fixing CIDs 1172014 and 1172013: Initializing members of GetProofCommand and ...Tim King
2017-09-26CID 1362904: Initializing GetInstantiationsCommand::d_smtEngine to nullptr. (...Tim King
2017-09-24CID 1362907: Initializing d_smtEngine to nullptr. (#1134)Tim King
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
2017-09-14Simplifying the throw specifier of SmtEngine::checkSat and related calls to C...Tim King
2017-09-13Floating point symfpu support (#1093)Martin
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
2017-08-25Move LFSC checker out of the CVC repository. (#222)Aina Niemetz
2017-08-23Fix typosAndres Noetzli
2017-08-14Move function defns from smt_engine_scope.h to cpp (#216)Andres Noetzli
2017-08-14Build and test suite fixes for Windows (#186)Mark Laws
2017-08-07Make quantifier elimination more robust to preprocessing.ajreynol
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-19Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Rem...Tim King
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ...ajreynol
2017-07-10Do not exit when value/model/unsat-core/proof is requested at wrong time, for...ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-05-31Fix model construction for BV with cbqi. Minor change to defaults.ajreynol
2017-05-31Minor change to defaults, update smt comp script, minor changes to options in...ajreynol
2017-05-15Fix bug 806. Minor fixes to remove term formula pass.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback