summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Collapse)Author
2017-03-02Eliminate 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-13Fix call to SExpr constructor for greater portability.Clark Barrett
2016-12-16Fix dependency tracing for fewerPreprocessingHolesAndres 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-07Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.ajreynol
2016-12-07Merge branch 'master' of https://github.com/CVC4/CVC4guykatzz
2016-12-07Turned off nonClausalSimplify when using fewerPreprocessingHoles.guykatzz
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure.
2016-12-07Refactoring, 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-05Added "dump=raw-benchmark" option for dumping all user commands exactly as ↵Clark Barrett
received.
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.ajreynol
2016-11-21Refactoring related to track instantiation option.ajreynol
2016-11-18Add support for set-logic ALL, fix compiler error in GCC 6.1Clark Barrett
2016-11-11Enable eager bitblasting for QF_ABV when no stores are present.Clark Barrett
2016-11-10Add option for enabling/disabling lazy extended function reduction in ↵ajreynol
bitvectors.
2016-11-08Add a few options to separation logic and sets. Minor changes to separation ↵ajreynol
logic, change syntax for empty heap constraint.
2016-11-04Fix a few more minor memory leaks.ajreynol
2016-11-02Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ajreynol
Fix a few more memory leaks.
2016-11-01Fix memory leak in TheorySetsRels. Minor cleanup.ajreynol
2016-11-01Revert change to Datatypes API to return vector of DatatypeTypes, as before. ↵ajreynol
ASAN failures with datatypes should now be mostly fixed.
2016-11-01Revert change to datatypes API for passing pointers, instead make deep copy ↵ajreynol
during call to mkMutualDatatypes.
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-31Minor refactoring in preparation for datatypes node cycle breaking.ajreynol
2016-10-28Add get instantiations utilities to API.ajreynol
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ajreynol
as extension of sets solver, add regressions.
2016-09-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by ↵ajreynol
default in EPR mode.
2016-09-12Refactor prenex modes.ajreynol
2016-09-12Remove old implementation of cbqiajreynol
2016-09-09Support 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-03Miniscope top level conjunctions for prenex normal form, allow one level ↵ajreynol
miniscoping in prenex normal form.
2016-09-03Option for prenex normal formajreynol
2016-09-01Cleanup quantifier elimination in smt engine.ajreynol
2016-09-01Updates 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-25Minor cleanup preprocessing, add ppNotifyAssertions.ajreynol
2016-08-19Fixed two bugsClark Barrett
2016-08-15Enable bounded set membership with --fmf-bound. Map to term models for ↵ajreynol
bounded set membership.
2016-08-11Add support for fewer preprocessing holesAndres 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-20Infrastructure 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-07Refactoring 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-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-06-20Addressed 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-20Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-20Fixed a bug where the proofManager's init() call was not getting called, ↵Guy
resutling a null point deference
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-06Merge pull request #85 from CVC4/master_for_proof_mergeguykatzz
Merge from proof branch
2016-06-03Simple memory fixes, minor cleanup in quantifiers.ajreynol
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01Merging proof branchGuy
2016-05-27Enabled bit-blasting option for QF_UFBVClark Barrett
2016-05-26Updated script, fixed bug in QF_NIA conversion.Clark Barrett
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. ↵ajreynol
Minor fixes for inst max level.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback