Age | Commit message (Collapse) | Author | |
---|---|---|---|
2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of ↵ | Liana Hadarean | |
Morgan's proof branch). | |||
2015-04-22 | Merge pull request #73 from kbansal/parser-dont-tokenize | Kshitij Bansal | |
Parser dont tokenize | |||
2015-04-21 | Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions. | ajreynol | |
2015-04-21 | Adding an example of a tester in SMT2. | Tim King | |
2015-04-17 | Patch for Kshitij's fix on requriePhase | Tianyi Liang | |
2015-04-17 | Merge pull request #72 from kbansal/decision-requirephase | Kshitij Bansal | |
https://www.starexec.org/starexec/secure/details/job.jsp?id=6972 The plot is bit misleading. Those not on x=y, are from QF_BV/asp which are segfaulting (see bugzilla 623). No performance impact on other logics it was tested on. | |||
2015-04-16 | disable failing sygus tests | Kshitij Bansal | |
2015-04-15 | Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2 | Tim King | |
2015-04-15 | Adding an example that violates an assertion during unconstrained ↵ | Tim King | |
simplification. | |||
2015-04-09 | disable string reqressions timing out after change | Kshitij Bansal | |
2015-03-23 | Parsing support for define-fun-rec/define-funs-rec. | ajreynol | |
2015-03-10 | CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵ | ajreynol | |
signature. Add regressions. | |||
2015-02-26 | Robust strategy for single invocation LIA synthesis conjectures. Add ↵ | ajreynol | |
regressions. | |||
2015-02-14 | Fix unit tests. | ajreynol | |
2015-02-13 | Handle recursive singleton case for codatatypes, add regression. Simplify ↵ | ajreynol | |
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes. | |||
2015-02-05 | Minor clean up | Tianyi Liang | |
2015-02-05 | Improved string performance, thanks to Peter's benchmarks. | Tianyi Liang | |
2015-01-20 | Mark datatypes as sygus. Add option to normalize sygus terms in search. ↵ | ajreynol | |
Add sygus regressions. | |||
2015-01-19 | Adding tests for get-value output for arithmetic. | Tim King | |
Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report. | |||
2015-01-14 | sygus input language and benchmark | Morgan Deters | |
2015-01-11 | adjusted to both v2.0 and v2.5 string literals | Tianyi Liang | |
2015-01-09 | blocked unprintable characters in string literals; | Tianyi Liang | |
disabled string literal test case for smtlib v2.5 | |||
2015-01-07 | bug fix, thanks to Pierre's report | Tianyi Liang | |
2014-12-28 | Disable prenex by default when using fmf bound int, minor improvement to ↵ | ajreynol | |
datatypes rewriter | |||
2014-12-04 | Relaxed the constant requirement for regular expression loop; | Tianyi Liang | |
Added "ignoring negative membership" option (fragment checking is not provided, and users must make sure the constraint is in the fragment; otherwise, the solution may not be correct). | |||
2014-12-03 | Floating point infrastructure. | Martin Brain | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-11-26 | add intersection rewriting | Tianyi Liang | |
2014-11-21 | Throw error when pattern is not list of terms. | ajreynol | |
2014-11-21 | Change default option to --inst-when=full-last-call (interleave ↵ | ajreynol | |
instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs. | |||
2014-11-20 | Disable constants sharing in eq engine, disable hack in theory engine. ↵ | ajreynol | |
Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine. | |||
2014-11-18 | Compute model basis only for fmf. Add another co-datatype regression. | ajreynol | |
2014-11-18 | Add local theory extensions instantiation strategy (incomplete). Refactor ↵ | ajreynol | |
how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist. | |||
2014-11-17 | Resource-limiting work. | Liana Hadarean | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-11-10 | Bug 593 fix: if the type is finite, it is now considered for detecting ↵ | Dejan Jovanović | |
theories of nested terms. | |||
2014-11-09 | Merge branch '1.4.x' | Morgan Deters | |
2014-11-09 | Increase stack size when running regressions (fixes some regression crashes ↵ | Morgan Deters | |
on Mac). | |||
2014-11-09 | Fix dt shared terms issue, reenable regression. | ajreynol | |
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. |