summaryrefslogtreecommitdiff
path: root/src/parser/smt2
AgeCommit message (Expand)Author
2014-06-29sets: "insert" operatorKshitij Bansal
2014-06-25make emptyset construction with no arguments privateKshitij Bansal
2014-06-25rename subseteq to subset in smtlib, all kinds and smt operator names are now...Kshitij Bansal
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij Bansal
2014-06-19Better error for invalid concrete syntax of sorts with too many parens, like ...Morgan Deters
2014-06-09Merge pull request #29 from kbansal/alternatefixKshitij Bansal
2014-06-08Previous "repeat" fix required extra lookahead (leading to assert-fails). Fi...Morgan Deters
2014-06-08smt2 parser: tokenize emptyset only if theory enabledKshitij Bansal
2014-06-08Better error when there are \backslashes in |quoted symbols|.Morgan Deters
2014-06-08Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).Morgan Deters
2014-06-04SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor,...Morgan Deters
2014-05-13Reject native extended ASCII characters. It requires user to use escaped sequ...Tianyi Liang
2014-04-29Fix for --force-logic to extend its reach to the parser.Morgan Deters
2014-04-24Add --inst-max-level=N option for Kshitij. Support define-const command in S...Andrew Reynolds
2014-04-14Add initial support for co-datatypes.Andrew Reynolds
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-04-09Handle fmf.card as input from user, add support in SMT2 parser, as requested ...Andrew Reynolds
2014-03-31add str to u16/u32, and u16/u32 to strTianyi Liang
2014-03-27adds new feature: re.loopTianyi Liang
2014-03-19Minor usability fixes related to SMT-LIB compliance.Morgan Deters
2014-03-14SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). Tha...Morgan Deters
2014-03-05Don't tokenize SET_THEORY operators in smt2 parserKshitij Bansal
2014-02-28add re.nostr for the empty regular expression; add re.allchar for the regular...Tianyi Liang
2014-02-28a new regular expression engine for solving both positive and negative member...Tianyi Liang
2014-02-28rename kind::IN to kind::MEMBER (fixes some windows build conflicts)Kshitij Bansal
2014-02-26smt-lib syntax change: str.contain -> str.contains; add some prefix syntax fo...Tianyi Liang
2014-02-25Minor code clean up in parser.Morgan Deters
2014-02-21add new theory (sets)Kshitij Bansal
2014-02-20add negative int2strTianyi Liang
2014-02-17type conversionTianyi Liang
2014-02-11lexer fix: disable smt-lib conversion for string literalsTianyi Liang
2014-02-06Minor fix for previous commitMorgan Deters
2014-02-06Oops.. premature push on lexer fix (remove debugging output)Morgan Deters
2014-02-06Fixes for escape-handling for string literals in SMT-LIBv2 lexerMorgan Deters
2014-01-29add prefixof, suffixofTianyi Liang
2014-01-09add constant replace, indexofTianyi Liang
2014-01-02Merge branch '1.3.x'Morgan Deters
2014-01-02Update copyright year.Morgan Deters
2013-12-27minor fixTianyi Liang
2013-12-27Merge branch '1.3.x'Morgan Deters
2013-12-27Fix for ANTLR warning.Morgan Deters
2013-12-26new functions in stringsTianyi Liang
2013-12-24Better get-value parse error message for common user error.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-02Minor cleanup.Morgan Deters
2013-11-11Expanded usefulness of (set-info :cvc4-logic ...)Morgan Deters
2013-10-20adds regular expression rangeTianyi Liang
2013-10-01adds partial function substr. the use of this function should be guarded, esp...Tianyi Liang
2013-10-01Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535Andrew Reynolds
2013-09-27removes unsound cases, adds unrollingTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback