Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-10-03 | Fix output of integer-valued real constants in SMT-LIB models (thanks ↵ | Morgan Deters | |
Christoph Sticksel for reporting). | |||
2014-10-03 | Minor fixes to CVC printer. | Morgan Deters | |
2014-08-22 | Fix operator-printing issue in SMT2. | Morgan Deters | |
2014-07-10 | membership cvc token changed to `IS_IN' to avoid conflict with IN used for let | Kshitij Bansal | |
2014-07-09 | sets cvc printer | Kshitij Bansal | |
2014-07-01 | Update copyrights. | Morgan Deters | |
2014-06-30 | Merge pull request #47 from kbansal/sets | Kshitij Bansal | |
Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are: SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset* API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET (those marked with [*] have changed or been added, others are as earlier) In the set-logic string use FS to enable sets. A not-so-well-tested perl command for translating old benchmarks: perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; ' | |||
2014-06-29 | sets: "insert" operator | Kshitij Bansal | |
new™! support for (insert (X (Set X)) (Set X) :right-associative) from the finte sets theory prosoal. e.g., (insert 1 2 3 4 (singleton 5)) | |||
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-22 | Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3: | Morgan Deters | |
1. no decimals used for rational literals 2. queries/check-sats wrapped with PUSH/POP | |||
2014-06-22 | Minor cleanup stuff. | Morgan Deters | |
2014-06-21 | Some minor cleanup and documentation. | Morgan Deters | |
2014-06-19 | For casc : print models of functions rewritten by sort inference. | ajreynol | |
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-05 | When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary. | Morgan Deters | |
2014-06-04 | Add operator support (resolves bug #563). | Morgan Deters | |
2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ↵ | Andrew Reynolds | |
assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real. | |||
2014-04-29 | Fix simplify output for SMT2 printer. | Morgan Deters | |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for ↵ | Andrew Reynolds | |
incorrectly applied selector terms. | |||
2014-04-03 | Properly quote symbols in SMT-LIB printer. | Morgan Deters | |
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 | Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting. | Morgan Deters | |
2014-03-05 | Improving support for POW in arithmetic. Resolves bug 549. | Tim King | |
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 | New translation work, support Z3-str-style string constraints. | 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-18 | switch to total function str.to.int: maps invalid and non-digit strings to 0 | Tianyi Liang | |
2014-02-17 | type conversion | Tianyi Liang | |
2014-02-14 | partial function charat | Tianyi Liang | |
2014-01-29 | add prefixof, suffixof | Tianyi Liang | |
2014-01-28 | merge internal and user of charat & substr into one | Tianyi Liang | |
2014-01-18 | strings with new ideas | Tianyi Liang | |
2014-01-17 | Merge branch '1.3.x' | Morgan Deters | |
2014-01-17 | Fix for quote-escaping in smt2 printer | Morgan Deters | |
2014-01-16 | adds partial functions | Tianyi Liang | |
2014-01-15 | adds smt2 print for strings | Tianyi Liang | |
2013-12-24 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: NEWS | |||
2013-12-24 | Better automatic handling of output language setting. | Morgan Deters | |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line | |||
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters | |
2013-12-05 | Fixes related to parametric datatype printing. | Morgan Deters | |
2013-12-02 | SExpr pretty-printing for :all-options and :all-statistics. | Morgan Deters | |
2013-11-27 | General pre-release cleanup commit | Morgan Deters | |
* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing | |||
2013-11-26 | Fix a segfault in the printer infrastructure when called from API and no ↵ | Morgan Deters | |
language is set | |||
2013-11-19 | Add fair strategy for finite model finding multiple sorts --uf-ss-fair. | Andrew Reynolds | |