Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ | ajreynol | |
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. | |||
2017-01-13 | Fix call to SExpr constructor for greater portability. | Clark Barrett | |
2016-12-16 | Fix dependency tracing for fewerPreprocessingHoles | Andres Notzli | |
Previously, dependency tracing in `ite_removal.cpp` was only done with the `unsatCores` option but `fewerPreprocessingHoles` requires dependencies, too. This lead to errors during proof construction when `fewerPreprocessingHoles` was active. This commit fixes the condition and includes a test case that previously failed. Additionally, it fixes a similar issue in the theory engine. NOTE: this commit might not fix all instances of this problem. `smt_engine.cpp` turns certain flags off with `unsatCores`. Compatibility between those flags and `fewerPreprocessingHoles` needs to be checked separately. | |||
2016-12-07 | Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764. | ajreynol | |
2016-12-07 | Merge branch 'master' of https://github.com/CVC4/CVC4 | guykatzz | |
2016-12-07 | Turned off nonClausalSimplify when using fewerPreprocessingHoles. | guykatzz | |
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure. | |||
2016-12-07 | Refactoring, generalization of bounded inference module. Simplification of ↵ | ajreynol | |
rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions. | |||
2016-12-05 | Added "dump=raw-benchmark" option for dumping all user commands exactly as ↵ | Clark Barrett | |
received. | |||
2016-12-02 | Bug fixes and refactoring of parametric datatypes, add some regressions. | ajreynol | |
2016-11-21 | Refactoring related to track instantiation option. | ajreynol | |
2016-11-18 | Add support for set-logic ALL, fix compiler error in GCC 6.1 | Clark Barrett | |
2016-11-11 | Enable eager bitblasting for QF_ABV when no stores are present. | Clark Barrett | |
2016-11-10 | Add option for enabling/disabling lazy extended function reduction in ↵ | ajreynol | |
bitvectors. | |||
2016-11-08 | Add a few options to separation logic and sets. Minor changes to separation ↵ | ajreynol | |
logic, change syntax for empty heap constraint. | |||
2016-11-04 | Fix a few more minor memory leaks. | ajreynol | |
2016-11-02 | Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ | ajreynol | |
Fix a few more memory leaks. | |||
2016-11-01 | Fix memory leak in TheorySetsRels. Minor cleanup. | ajreynol | |
2016-11-01 | Revert change to Datatypes API to return vector of DatatypeTypes, as before. ↵ | ajreynol | |
ASAN failures with datatypes should now be mostly fixed. | |||
2016-11-01 | Revert change to datatypes API for passing pointers, instead make deep copy ↵ | ajreynol | |
during call to mkMutualDatatypes. | |||
2016-11-01 | Working memory leak free version, changes interface to pointers. | ajreynol | |
2016-10-31 | Minor refactoring in preparation for datatypes node cycle breaking. | ajreynol | |
2016-10-28 | Add get instantiations utilities to API. | ajreynol | |
2016-10-26 | New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ | ajreynol | |
as extension of sets solver, add regressions. | |||
2016-09-15 | Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by ↵ | ajreynol | |
default in EPR mode. | |||
2016-09-12 | Refactor prenex modes. | ajreynol | |
2016-09-12 | Remove old implementation of cbqi | ajreynol | |
2016-09-09 | Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵ | ajreynol | |
allow sep disequal card constants when type is monotonic. Update logics on sep regressions. | |||
2016-09-03 | Miniscope top level conjunctions for prenex normal form, allow one level ↵ | ajreynol | |
miniscoping in prenex normal form. | |||
2016-09-03 | Option for prenex normal form | ajreynol | |
2016-09-01 | Cleanup quantifier elimination in smt engine. | ajreynol | |
2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested ↵ | ajreynol | |
quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly. | |||
2016-08-25 | Minor cleanup preprocessing, add ppNotifyAssertions. | ajreynol | |
2016-08-19 | Fixed two bugs | Clark Barrett | |
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for ↵ | ajreynol | |
bounded set membership. | |||
2016-08-11 | Add support for fewer preprocessing holes | Andres Notzli | |
This commit adds support for the --fewer-preprocessing-holes flag. This flag changes the preprocessing part in proofs in two ways: it (1) removes assertions that are just restating inputs and uses the inputs directly instead and it (2) changes the form of the preprocessed assertions to contain the input that they originate from. The code in this commit is mostly taken from the proofs branch in Guy's fork. | |||
2016-07-20 | Infrastructure for storing and printing heap models for separation logic. ↵ | ajreynol | |
Ensure value of sep.nil is correct in models. Print instantiations as sexprs. | |||
2016-07-07 | Refactoring of strings preprocess module. When enabled, apply eager ↵ | ajreynol | |
preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep. | |||
2016-07-06 | Add comment field for model, resolves hack for printing sep logic models. | ajreynol | |
2016-06-20 | Addressed a bug that occurs when proof production is triggered via text ↵ | Guy | |
flags in the input. Separated some initialization into two phases: 1. Those that can be done when the proof compiliation flag is set 2. Those that can be done only when the --proof option is set. For #2, deferred their execution until the text flags in the input have been processed | |||
2016-06-20 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-06-20 | Fixed a bug where the proofManager's init() call was not getting called, ↵ | Guy | |
resutling a null point deference | |||
2016-06-17 | Support for separation logic. Enable cbqi by default for pure BV. | ajreynol | |
2016-06-06 | Merge pull request #85 from CVC4/master_for_proof_merge | guykatzz | |
Merge from proof branch | |||
2016-06-03 | Simple memory fixes, minor cleanup in quantifiers. | ajreynol | |
2016-06-01 | Merge from proof branch | Guy | |
2016-06-01 | Revert "Merging proof branch" | Guy | |
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8. | |||
2016-06-01 | Merging proof branch | Guy | |
2016-05-27 | Enabled bit-blasting option for QF_UFBV | Clark Barrett | |
2016-05-26 | Updated script, fixed bug in QF_NIA conversion. | Clark Barrett | |
2016-05-18 | Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. ↵ | ajreynol | |
Minor fixes for inst max level. |