| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-07 | Properly distinguish which EQC to assign values in datatypes, use ↵ | ajreynol | |
| assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure. | |||
| 2014-11-06 | Reenable regression. Add (for now, disabled) changes to datatypes theory ↵ | ajreynol | |
| combination. Relax communication of dt facts. | |||
| 2014-11-05 | More work on datatypes theory combination: fix bug in care graph, do not ↵ | ajreynol | |
| assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes. | |||
| 2014-11-01 | Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in ↵ | ajreynol | |
| lemmas being rewritten). Minor improvement to dt care graph. Reenable regressions. | |||
| 2014-11-01 | Fix some mistakes in datatypes theory combination, disable two regressions. ↵ | ajreynol | |
| Minor fix for fun defs. | |||
| 2014-10-31 | Do not allow duplication of function definitions. Set incomplete flag in ↵ | ajreynol | |
| model builder. | |||
| 2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters | |
| * support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.) | |||
| 2014-10-22 | Fix bug590 regression distcheck failure from last night. | Morgan Deters | |
| 2014-10-21 | Fixed bug 590, added regression test | Clark Barrett | |
| 2014-10-10 | Merge remote-tracking branch 'origin/1.4.x' | Kshitij Bansal | |
| 2014-10-10 | Fix issue with shared but non-preregistered term setup. Thanks Alvise ↵ | Kshitij Bansal | |
| Rabitti for the report. | |||
| 2014-10-06 | Merge branch '1.4.x' | Morgan Deters | |
| 2014-10-06 | Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report. | Morgan Deters | |
| 2014-10-06 | Merge branch '1.4.x' | Morgan Deters | |
| 2014-10-06 | fix for bug586 | Kshitij Bansal | |
| 2014-10-06 | Extended parsing testcase, with constant arrays and RESET. | Morgan Deters | |
| 2014-10-06 | Merge branch '1.4.x' | Morgan Deters | |
| Conflicts: test/regress/regress0/arrays/Makefile.am | |||
| 2014-10-06 | Fix native language parsing of chained-store expressions (resolves bug 585). ↵ | Morgan Deters | |
| Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic. | |||
| 2014-10-04 | Enable some old bug testcases that (maybe?) never got added. | Morgan Deters | |
| 2014-10-03 | Add some (so far trivial) regressions for constant arrays. | Morgan Deters | |
| 2014-09-24 | Fix infinite loop in datatypes enumerator. Minor work on conjecture generator. | ajreynol | |
| 2014-09-17 | Fix soundness bug for quantifier macros involving Int/Real. | ajreynol | |
| 2014-09-03 | Implement and enable --dt-var-exp-quant, cleanup trace messages, minor ↵ | ajreynol | |
| changes for relevant term filtering. | |||
| 2014-08-28 | fixing bug580 caused by bad bv inequality explanation | lianah | |
| 2014-08-28 | fixing bug580 caused by bad bv inequality explanation | lianah | |
| 2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters | |
| 2014-08-22 | Merge branch '1.4.x' | Morgan Deters | |
| 2014-08-22 | Fix incorrectly-labeled test. | Morgan Deters | |
| 2014-08-18 | Merge branch '1.4.x' | Morgan Deters | |
| Conflicts: test/regress/regress0/Makefile.am | |||
| 2014-08-18 | Revert a8e0ce67 and add test case (resolves bug #578). | Morgan Deters | |
| This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb. | |||
| 2014-08-04 | Some fixes to symmetry breaker (resolves bug 576). | Morgan Deters | |
| 2014-08-04 | Some fixes to symmetry breaker (resolves bug 576). | Morgan Deters | |
| 2014-07-25 | patch for regular expression intersection caching | Tianyi Liang | |
| 2014-07-21 | run_regression using valgrind by setting VALGRIND=1 | Kshitij Bansal | |
| 2014-07-12 | Status for new bug testcase. | Morgan Deters | |
| 2014-07-12 | Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre ↵ | Morgan Deters | |
| for the report. | |||
| 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 parser | Kshitij Bansal | |
| 2014-07-09 | sets cvc printer | Kshitij Bansal | |
| 2014-06-30 | Merge pull request #45 from mdeters/turn-off-strings-exp | Morgan Deters | |
| Turn strings-exp off by default (for the release) | |||
| 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 | Turn strings-exp off by default (for the release) | Morgan Deters | |
| 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 | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback