summaryrefslogtreecommitdiff
path: root/src/parser/smt2
AgeCommit message (Expand)Author
2019-05-06Add support for re.all (#2980)Andres Noetzli
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-25New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)Aina Niemetz
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-04-16Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)Andres Noetzli
2019-03-26Update copyright headers.Aina Niemetz
2019-03-19Make declare-datatype(s) a standard, non-extended command in the Smt2 parser....Andrew Reynolds
2019-03-18New C++: Remove redundant mkVar function.Aina Niemetz
2019-01-10New C++ API: Get rid of mkConst functions (simplify API). (#2783)Aina Niemetz
2019-01-03API/Smt2 parser: refactor termAtomic (#2674)Andres Noetzli
2018-11-27Reduce lookahead when parsing string literals (#2721)Andres Noetzli
2018-11-21Support string replace all (#2704)Andrew Reynolds
2018-10-20Remove antlr_undefines.h. (#2664)Mathias Preiner
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-10-02Allow (_ to_fp ...) in strict parsing mode (#2566)Andres Noetzli
2018-09-26Makes SyGuS parsing more robust in invariant problems (#2509)Haniel Barbosa
2018-09-22cmake: Only build libcvc4 and libcvc4parser as libraries.Mathias Preiner
2018-09-22cmake: Move find_package to where it is actually needed.Mathias Preiner
2018-09-22cmake: Cleanup CMakeLists.txt files, remove SHARED.Mathias Preiner
2018-09-22cmake: Working build infrastructure.Mathias Preiner
2018-09-22cmake: Antlr parser generation done.Mathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-27Make division chainable in the smt2 parser (#2367)Andrew Reynolds
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-20 Remove support for prototype (non-sygus) synthesis (#2338)Andrew Reynolds
2018-08-17Split sygus grammar to its own ANTLR grammar (#2307)Andrew Reynolds
2018-08-08Plug solver API object into parser. (#2240)Aina Niemetz
2018-08-07Simplify and improve the sygus parser (#2266)Andrew Reynolds
2018-08-06Add RegLan to smt2/sygus parsers. (#2276)Andrew Reynolds
2018-08-06Remove support for Enum sygus syntax. (#2264)Andrew Reynolds
2018-08-02Parse standard separation logic inputs (#2257)Andrew Reynolds
2018-08-01Fix issues with printing parametric datatypes in smt2 (#2213)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-29 Make user's SMT2 version override file version (#2004)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-21Improvements in parsing and printing related to mixed int/real (#1879)Andrew Reynolds
2018-05-08Support for str.<= and str.< (#1882)Andrew Reynolds
2018-05-07Add support for str.code (#1821)Andrew Reynolds
2018-05-03Fix redundant internalPush calls. (#1865)Mathias Preiner
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-04-08Check free variables in assertions (#1737)Andrew Reynolds
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
2018-03-05Add support for check-sat-assuming. (#1637)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback