summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
AgeCommit message (Expand)Author
2018-08-21 Fix processing of nested Variable construct in sygus let bodies (#2351)Andrew Reynolds
2018-08-21Warn and enable quantifiers when using sygus + logics with QF (#2352)Andrew Reynolds
2018-08-08Plug solver API object into parser. (#2240)Aina Niemetz
2018-08-06Add RegLan to smt2/sygus parsers. (#2276)Andrew Reynolds
2018-07-14sygusComp2018: update semantics for declare-fun in sygus. (#2102)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-04Only enable transcendentals if logic is N[I]RAT (#2052)Andres Noetzli
2018-05-29Track input language in a single place (#2003)Andres Noetzli
2018-05-22Parse error for sygus grammar term with multiple let bodies (#1961)Andrew Reynolds
2018-05-08Support for str.<= and str.< (#1882)Andrew Reynolds
2018-05-07Add support for str.code (#1821)Andrew Reynolds
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
2018-02-27Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)Aina Niemetz
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2017-12-27Rel smt parser (#1446)Arjun Viswanathan
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
2017-12-01Refactor and generalize PBE strategies (#1410)Andrew Reynolds
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-11-05Make higher-order a flag in logic info. (#1318)Andrew Reynolds
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
2017-10-12Sygus logics (#1226)Andrew Reynolds
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-03Op overload parser (#1162)Andrew Reynolds
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
2017-08-25Added missing includes (algorithm).Aina Niemetz
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring of...ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-07-05Non-linear supported in ALL logics. Minor fixes for set logic with sygus.ajreynol
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil no...ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-11-18Add support for set-logic ALL, fix compiler error in GCC 6.1Clark Barrett
2016-11-01Revert change to datatypes API for passing pointers, instead make deep copy d...ajreynol
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-09-14Support for unique variable generation in node manager.ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize irre...ajreynol
2016-04-20update from the masterPaulMeng
2016-04-15change transitive closure operator name to TCLOUSREPaulMeng
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
2016-04-03Updating the copyright headers and scripts.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback