Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-06-25 | make emptyset construction with no arguments private | Kshitij Bansal | |
2014-06-25 | rename subseteq to subset in smtlib, all kinds and smt operator names are ↵ | Kshitij Bansal | |
now consistent | |||
2014-06-22 | Renaming of SMT2 operator names, kinds for set theory | Kshitij Bansal | |
* SET_SINGLETON kind renamed to just SINGLETON * "setenum" smt2 opertor renamed to "singleton"[1] * "in" smt2 operator renamed to "member"[2] [1] It was anyhow accepting exactly one argument, so was bit misleading to call set enumerator. [2] The corresponding kind was called MEMBER, so this will also make them consistent. Only inconsistency now is for subset: kind is called SUBSET but operator is called "subseteq". | |||
2014-06-19 | Better error for invalid concrete syntax of sorts with too many parens, like ↵ | Morgan Deters | |
(Int). Thanks to Dan Liew for the report. | |||
2014-06-09 | Merge pull request #29 from kbansal/alternatefix | Kshitij Bansal | |
Fix for emptyset in smt2 parser, sets translator to quantified logic, misc | |||
2014-06-08 | parseErrorHelper : factor out whole word matching | Kshitij Bansal | |
catches some corner cases, more readable too | |||
2014-06-08 | Previous "repeat" fix required extra lookahead (leading to assert-fails). ↵ | Morgan Deters | |
Fixed, at the cost of an antlr warning that's safe to ignore for now. | |||
2014-06-08 | smt2 parser: tokenize emptyset only if theory enabled | Kshitij Bansal | |
2014-06-08 | Better error when there are \backslashes in |quoted symbols|. | Morgan Deters | |
2014-06-08 | Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this). | Morgan Deters | |
2014-06-06 | Sets translate, and other short fixes | Kshitij Bansal | |
- $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine | |||
2014-06-04 | Add operator support (resolves bug #563). | Morgan Deters | |
2014-06-04 | SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, ↵ | Morgan Deters | |
bvor, and bvxor. | |||
2014-05-13 | Reject native extended ASCII characters. It requires user to use escaped ↵ | Tianyi Liang | |
sequence for an extended ASCII character. | |||
2014-04-29 | Fix for --force-logic to extend its reach to the parser. | Morgan Deters | |
2014-04-29 | fix was compiler warning in antlr_input, crashing test case with the old fix | Kshitij Bansal | |
2014-04-29 | Revert a compiler warning fix from ea6a5a6. | Morgan Deters | |
2014-04-29 | fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr | Tianyi Liang | |
2014-04-28 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal | |
2014-04-27 | attempt to improve CVC4's "parse error" message | Kshitij Bansal | |
2014-04-24 | Add --inst-max-level=N option for Kshitij. Support define-const command in ↵ | Andrew Reynolds | |
Smt2. | |||
2014-04-14 | Add initial support for co-datatypes. | Andrew Reynolds | |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for ↵ | Andrew Reynolds | |
incorrectly applied selector terms. | |||
2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵ | Andrew Reynolds | |
Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit. | |||
2014-04-09 | Handle fmf.card as input from user, add support in SMT2 parser, as requested ↵ | Andrew Reynolds | |
by Martin Brain. Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental. | |||
2014-04-04 | For security, add --no-filesystem-access option, which disables SMT-LIB ↵ | Morgan Deters | |
script access to filesystem. | |||
2014-03-31 | add str to u16/u32, and u16/u32 to str | Tianyi Liang | |
2014-03-27 | adds new feature: re.loop | Tianyi Liang | |
2014-03-19 | Minor usability fixes related to SMT-LIB compliance. | Morgan Deters | |
2014-03-14 | SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). ↵ | Morgan Deters | |
Thanks to David Cok for the bug report. | |||
2014-03-05 | Don't tokenize SET_THEORY operators in smt2 parser | Kshitij Bansal | |
2014-02-28 | add re.nostr for the empty regular expression; add re.allchar for the ↵ | Tianyi Liang | |
regular expresssion containing all charactors | |||
2014-02-28 | a new regular expression engine for solving both positive and negative ↵ | Tianyi Liang | |
membership constraints | |||
2014-02-28 | rename kind::IN to kind::MEMBER (fixes some windows build conflicts) | Kshitij Bansal | |
2014-02-26 | smt-lib syntax change: str.contain -> str.contains; add some prefix syntax ↵ | Tianyi Liang | |
for cvc format | |||
2014-02-25 | Minor code clean up in parser. | Morgan Deters | |
2014-02-21 | add new theory (sets) | Kshitij Bansal | |
Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment | |||
2014-02-20 | add negative int2str | Tianyi Liang | |
2014-02-20 | String parsing example in CVC parser | Morgan Deters | |
2014-02-17 | type conversion | Tianyi Liang | |
2014-02-11 | lexer fix: disable smt-lib conversion for string literals | Tianyi Liang | |
2014-02-06 | Minor fix for previous commit | Morgan Deters | |
2014-02-06 | Oops.. premature push on lexer fix (remove debugging output) | Morgan Deters | |
2014-02-06 | Fixes for escape-handling for string literals in SMT-LIBv2 lexer | Morgan Deters | |
2014-01-29 | add prefixof, suffixof | Tianyi Liang | |
2014-01-09 | add constant replace, indexof | Tianyi Liang | |
2014-01-02 | Merge branch '1.3.x' | Morgan Deters | |
2014-01-02 | Update copyright year. | Morgan Deters | |
2013-12-27 | minor fix | Tianyi Liang | |
2013-12-27 | Merge branch '1.3.x' | Morgan Deters | |