Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-11-08 | Fix bug with incremental+datatypes. Minor cleanup. Disable regression ↵ | ajreynol | |
bug484, enable parsing_ringer. | |||
2014-11-07 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: src/smt/model_postprocessor.cpp test/regress/regress0/Makefile.am | |||
2014-11-07 | Fix missing case in Boolean terms rewriting. (Resolves bug #596.) | Morgan Deters | |
2014-11-07 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: src/smt/model_postprocessor.cpp | |||
2014-11-07 | Corrected fix for missing case in model postprocessor (resolves bug #595). | Morgan Deters | |
2014-11-07 | Revert "Fix missing case in model postprocessor (resolves bug #595)." | Morgan Deters | |
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. | |||
2014-11-07 | Revert "Fix missing case in model postprocessor (resolves bug #595)." | Morgan Deters | |
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. Conflicts: test/regress/regress0/Makefile.am | |||
2014-11-07 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: test/regress/regress0/Makefile.am | |||
2014-11-07 | Fix missing case in model postprocessor (resolves bug #595). | Morgan Deters | |
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-17 | Merge branch '1.4.x' | Morgan Deters | |
2014-10-17 | Remove a bad (unstable, timing-dependent) test. | Morgan Deters | |
2014-10-14 | Context-dependent expr attributes are now attached to a specific SmtEngine, ↵ | Morgan Deters | |
and the SAT context is owned by the SmtEngine. | |||
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 | Fix unit test that was broken with last commit. | Morgan Deters | |
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-10-03 | Merge branch '1.4.x' | Morgan Deters | |
2014-10-03 | Fix unit test for ArrayStoreAll. | Morgan Deters | |
2014-09-25 | fix unit test for new fair datatype enumeration | 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 | Unit test fix. | Morgan Deters | |
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-08-04 | Better support for resource-limiting when there aren't any actual conflicts. | Morgan Deters | |