Age | Commit message (Collapse) | Author | |
---|---|---|---|
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-30 | Use FS as the set-logic string for theory of sets | Kshitij Bansal | |
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-27 | Fix for bug543 | Clark Barrett | |
2014-06-25 | rename subseteq to subset in smtlib, all kinds and smt operator names are ↵ | Kshitij Bansal | |
now consistent | |||
2014-06-23 | Fatal error if --unconstrained-simp and --produce-models used together ↵ | Morgan Deters | |
(before it would just override the user and turn off models). | |||
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 | forgot to add the test with fix | Kshitij Bansal | |
according to bug report, fix was in 6267f3 | |||
2014-06-19 | disable unate lemmas when using incremental mode | Kshitij Bansal | |
2014-06-13 | fixed BVMinisat bug due to not clearing seen properly | lianah | |
2014-06-11 | disable another test, after recent merges taking too long | Kshitij Bansal | |
2014-06-11 | sets: comment out an assertion too strong | Kshitij Bansal | |
2014-06-11 | user/sat context issue in sets | Kshitij Bansal | |
2014-06-11 | fix in sets rewriter | Kshitij Bansal | |
2014-06-10 | Merging CAV14 paper bit-vector work. | lianah | |
2014-06-08 | test for prvs commit (tokenize emptyset) | Kshitij Bansal | |
9978c259f30b1f4b2c70c04589a309033a6eb1f6 | |||
2014-06-06 | Merge pull request #28 from kbansal/sets | Kshitij Bansal | |
Sets translator, bug fixes | |||
2014-06-06 | Patch for the subtype theoryof mode to make the equalities over disequal ↵ | Tim King | |
types get sent to the theory of the type. Adding a new test case for bug 569. Fixes to the normal form of arithmetic so that real terms are before integer terms. | |||
2014-06-06 | sets: fix equality propagation | Kshitij Bansal | |
2014-05-25 | Improve quantifier instantiation: always use original terms when matching ↵ | Andrew Reynolds | |
(was missing for simple triggers). Minor updates to scripts. | |||
2014-05-23 | Fix bug in E-matching Real/Int terms. | Andrew Reynolds | |
2014-05-16 | sets: fix a bug in model building, another in handling set of sets | Kshitij Bansal | |
2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ↵ | ajreynol | |
Add regressions. | |||
2014-05-12 | Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report. | Tianyi Liang | |
2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, ↵ | Andrew Reynolds | |
minor changes. | |||
2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King | |
This commit includes work from the past month on the T-entailment check infrastructure (due to Tim), an entailment check for arithmetic (also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds). Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-04-29 | fix was compiler warning in antlr_input, crashing test case with the old fix | Kshitij Bansal | |
2014-04-29 | add leading zeros support for str.to.int | Tianyi Liang | |
2014-04-28 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal | |
2014-04-28 | travis, please! | Kshitij Bansal | |
2014-04-27 | attempt to improve CVC4's "parse error" message | Kshitij Bansal | |
2014-04-14 | Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ↵ | Andrew Reynolds | |
Improve datatypes rewrite, make option for previous dt semantics. | |||
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 | add tests | Kshitij Bansal | |
2014-04-09 | inputs to trigger bug | Kshitij Bansal | |
2014-04-06 | Reduced example from pcc's bug report. | Tim King | |
2014-04-06 | Merge pull request #21 from pcc/ite-fix | Tim King | |
Fix for ite of >=64bit wide bitvectors with unconstrained condition. | |||
2014-04-03 | Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis ↵ | Morgan Deters | |
Deligiannis and Jeroen Ketema for discovering this issue. | |||
2014-03-31 | add str to u16/u32, and u16/u32 to str | Tianyi Liang | |
2014-03-28 | add construles, type_rules rm redundant, kinds cleanup | Kshitij Bansal | |
2014-03-27 | adds new feature: re.loop | Tianyi Liang | |
2014-03-20 | Merge pull request #22 from kbansal/sets-model | Kshitij Bansal | |
Sets model | |||
2014-03-20 | cleanup | Kshitij Bansal | |
2014-03-20 | fix for sets/mar2014/..317minimized.. | Kshitij Bansal | |
Observed behavior: --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) with different set of elements in the model for representative and the node itself. Issue: The trouble with data structure being mainted to ensure that things for which lemmas have been generated are not generated again. This data structure (d_pendingEverInserted) needs to be user context dependent. The bug was in the sequence of steps from requesting that a lemma be generated to when it actually was. Sequence was: addToPending (and also adds to pending ever inserted) -> isComplete (might remove things from pending if requirment met in other ways) -> getLemma (actually generated the lemma, if requirement not already met) Resolution: adding terms to d_pendingEverInserted was moved from addToPending() to getLemma(). | |||
2014-03-20 | Fix for registration issues of term appearing in a shared lemma | Kshitij Bansal | |
(brought to attention by lianah -- fix currently just adapted using arrays -- this is to remind me to raise why do we even have this isPreregistered bussiness) | |||
2014-03-20 | fix a sharing issues with sets | Kshitij Bansal | |
2014-03-20 | enable check-models for sets/ regressions | Kshitij Bansal | |
2014-03-20 | testlemma regressions | Kshitij Bansal | |
2014-03-19 | Minor usability fixes related to SMT-LIB compliance. | Morgan Deters | |