summaryrefslogtreecommitdiff
path: root/src/printer
AgeCommit message (Collapse)Author
2014-10-03Fix output of integer-valued real constants in SMT-LIB models (thanks ↵Morgan Deters
Christoph Sticksel for reporting).
2014-10-03Minor fixes to CVC printer.Morgan Deters
2014-08-22Fix operator-printing issue in SMT2.Morgan Deters
2014-07-10membership cvc token changed to `IS_IN' to avoid conflict with IN used for letKshitij Bansal
2014-07-09sets cvc printerKshitij Bansal
2014-07-01Update copyrights.Morgan Deters
2014-06-30Merge pull request #47 from kbansal/setsKshitij 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-29sets: "insert" operatorKshitij 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-25rename subseteq to subset in smtlib, all kinds and smt operator names are ↵Kshitij Bansal
now consistent
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij 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-22Output 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-22Minor cleanup stuff.Morgan Deters
2014-06-21Some minor cleanup and documentation.Morgan Deters
2014-06-19For casc : print models of functions rewritten by sort inference.ajreynol
2014-06-06Sets translate, and other short fixesKshitij 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-05When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary.Morgan Deters
2014-06-04Add operator support (resolves bug #563).Morgan Deters
2014-05-11More 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-29Fix simplify output for SMT2 printer.Morgan Deters
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for ↵Andrew Reynolds
incorrectly applied selector terms.
2014-04-03Properly quote symbols in SMT-LIB printer.Morgan Deters
2014-03-31add str to u16/u32, and u16/u32 to strTianyi Liang
2014-03-27adds new feature: re.loopTianyi Liang
2014-03-19Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.Morgan Deters
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2014-02-28add re.nostr for the empty regular expression; add re.allchar for the ↵Tianyi Liang
regular expresssion containing all charactors
2014-02-28a new regular expression engine for solving both positive and negative ↵Tianyi Liang
membership constraints
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 ↵Tianyi Liang
for cvc format
2014-02-25New translation work, support Z3-str-style string constraints.Morgan Deters
2014-02-21add 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-18switch to total function str.to.int: maps invalid and non-digit strings to 0Tianyi Liang
2014-02-17type conversionTianyi Liang
2014-02-14partial function charatTianyi Liang
2014-01-29add prefixof, suffixofTianyi Liang
2014-01-28merge internal and user of charat & substr into oneTianyi Liang
2014-01-18strings with new ideasTianyi Liang
2014-01-17Merge branch '1.3.x'Morgan Deters
2014-01-17Fix for quote-escaping in smt2 printerMorgan Deters
2014-01-16adds partial functionsTianyi Liang
2014-01-15adds smt2 print for stringsTianyi Liang
2013-12-24Merge branch '1.3.x'Morgan Deters
Conflicts: NEWS
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-23Proof-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-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-05Fixes related to parametric datatype printing.Morgan Deters
2013-12-02SExpr pretty-printing for :all-options and :all-statistics.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan 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-26Fix a segfault in the printer infrastructure when called from API and no ↵Morgan Deters
language is set
2013-11-19Add fair strategy for finite model finding multiple sorts --uf-ss-fair.Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback