Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-07-12 | Make type rules more strict for operators whose type rules involve subtypes. ↵ | ajreynol | |
Disable support for subrange and predicate subtypes (which were only partially supported previously). | |||
2017-07-10 | Add nl regression. | ajreynol | |
2017-07-10 | Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵ | ajreynol | |
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions. | |||
2017-07-10 | Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ | ajreynol | |
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions. | |||
2017-07-07 | Remove unused stacking_vector class (#185) | Andres Noetzli | |
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2017-07-05 | Fix for logic info, update regressions. Update casc tfa script. | ajreynol | |
2017-07-05 | Update unit test, news. | ajreynol | |
2017-07-05 | Non-linear supported in ALL logics. Minor fixes for set logic with sygus. | ajreynol | |
2017-06-30 | Minor change to trigger selection, fixes related to subtypes (in macros, ↵ | ajreynol | |
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts. | |||
2017-06-28 | Enable non-linear solve by default, update regressions. | ajreynol | |
2017-06-22 | Fix assertion failure due to missing clause id (#180) | Andres Nötzli | |
This commit fixes bug 821. As written in the description of the bug, the issue is that `id` is not being set on one of the paths in addClause(), specifically in the case where all but one literal are assigned false and the remaining literal is assigned true. In that case, we are not actually adding anything and set the `id` to `ClauseIdUndef`. | |||
2017-06-21 | Properly handle subtypes in smt2 printer. | ajreynol | |
2017-06-16 | Merge pull request #170 from CVC4/fix_2_6_parser3 | Clark Barrett | |
Parse 'is', 'match' differently for non-DT input | |||
2017-06-16 | Fix segfault by making unit conflict CDMaybe | Andres Nötzli | |
This commit fixes bug 819 by making d_unitConflictId context dependent and adds a test case. | |||
2017-06-16 | Parse 'is', 'match' differently for non-DT input | Andres Noetzli | |
In SMT 2.6, Datatypes are being introduced and they come with testers (indexed identifier of the form (_ is c)) and match expressions. This lead to failures in UFIDL benchmarks in SMT-LIB because they declare the function 'is'. This commit changes the parser s.t. it does not consider 'is' and 'match' special tokens unless the theory of datatypes is enabled. | |||
2017-06-15 | Fix for bug 639. | Clark Barrett | |
2017-06-15 | Add regression. | ajreynol | |
2017-06-02 | Fix regression. | ajreynol | |
2017-06-02 | Incorporate datatypes into smt comp script, add regression. | ajreynol | |
2017-05-31 | Fix model construction for BV with cbqi. Minor change to defaults. | ajreynol | |
2017-05-31 | Minor change to defaults, update smt comp script, minor changes to options ↵ | ajreynol | |
in regressions. | |||
2017-05-26 | Checking that equalities belong to the arithmetic theory in the solve() routine. | Tim King | |
2017-05-20 | Fix bug 812. | ajreynol | |
2017-05-15 | Cleanup handling of division (possible fix for bugs 803, 804, 805). | ajreynol | |
2017-05-15 | Merge pull request #158 from 4tXJ7f/fix_sets_rewriter | Andrew Reynolds | |
Fix minor bug in sets rewriter | |||
2017-05-15 | Fix minor bug in sets rewriter | Andres Noetzli | |
As reported by Coverity, one of the switches in the sets rewriter had a missing break. This could lead to an assertion failure when rewriting the cardinality of a transpose as in the test case included in this commit. | |||
2017-05-15 | Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802. | ajreynol | |
2017-05-13 | Fix out-of-bounds access in test | Andres Notzli | |
2017-05-12 | Make signal handlers safer | Andres Notzli | |
As reported in bug 769, the signal handlers currently use unsafe functions such as dynamic memory allocations and fprintf. This commit fixes the issue by introducing functions for printing statistics in signal handlers (functions with the `safe` prefix). It also avoids copying statistics, which further avoids dynamic memory allocation. The safe printing of statistics has some limitations (it does not support SExprStats or printing CVC4::Result), which should not matter much in practice. Printing statistics in a non-signal handler is not affected by these changes as that uses a separate code path (the functions without the `safe` prefix). Additional changes: - Remove ListStat as it is not used anywhere - Add unit test for safe printing statistics | |||
2017-05-10 | Do not split on cardinality for string equivalence classes with non-constant ↵ | ajreynol | |
lengths if disequalities already imply sufficient lower bound. Fixes bug 799. | |||
2017-05-09 | Change str.replace for empty string. | ajreynol | |
2017-05-05 | Do not eliminate extended arithmetic symbols when finite model finding is ↵ | ajreynol | |
on, add regression. | |||
2017-04-28 | Minor fixes | ajreynol | |
2017-04-28 | Fix bug for real division. | ajreynol | |
2017-04-28 | Do not eliminate non-standard arithmetic operators in recursive function ↵ | ajreynol | |
definitions, add regression. | |||
2017-04-24 | Fixes and simplifications for fmf mbqi. | ajreynol | |
2017-04-24 | Fix parsing selectors for nullary constructors in smtlib 2.6 format. | ajreynol | |
2017-04-23 | Changing spaces to tabs in Makefile. | Tim King | |
2017-04-21 | Disabled bug639.smt2 which still fails. | Clark Barrett | |
2017-04-21 | Add test cases for bugs 639 and 681. | Clark Barrett | |
2017-04-21 | Fix new relations regressions to use sets-ext. | ajreynol | |
2017-04-21 | Handle subtypes in sets. Bug fixes for tuples with subtypes. | ajreynol | |
2017-04-20 | Support for relational operators identity and join image | Paul Meng | |
2017-04-19 | Fixes for handling set universe: restrict upwards rule for universe to ↵ | ajreynol | |
memberships into variable sets, do not variable eliminate sets during ppAssert. | |||
2017-04-14 | Actively split for upwards closusure intersection. Minor clean up, add ↵ | ajreynol | |
regressions. | |||
2017-04-14 | Fix for fmf-fun when the option is set by user command. | ajreynol | |
2017-04-07 | Change option names for nl. | ajreynol | |
2017-04-05 | Merge pull request #143 from FabianWolff/master | Clark Barrett | |
Fix several spelling errors | |||
2017-04-05 | Fix bug 698. | ajreynol | |