Age | Commit message (Collapse) | Author | |
---|---|---|---|
2015-10-26 | This fixes a one definition rule violation for reduceDB_lt in Solver.cc in ↵ | Tim King | |
minisat and bvminisat. This also moves BVMinisat into CVC4. This also wrapped code in cpp files into the namespaces instead of having using namespace *. | |||
2015-10-26 | Promote InstStrategyCbqi to quantifier module. Cleanup unused code. | ajreynol | |
2015-10-26 | Extend counterexample-guided instantiation to extended theory of Int/Real, ↵ | ajreynol | |
mixed Int/Real. Bug fixes. Updates to quantifiers rewriter. | |||
2015-10-24 | Fixes related to string contains. | ajreynol | |
2015-10-23 | This removes a bug for reading data that has been popped from the back of a ↵ | Tim King | |
vector using a stale reference in the unconstrained simplifier. | |||
2015-10-23 | Specify that the default initialization must always be done for ↵ | Tim King | |
CDOhash_map's data field. Without doing this, there exists a loop where uninitialized data can be read. This can happen if T is a type like bool. The trace goes: CDOhash_map::set(data) calls ContextObj::make_current(). Now (d_pScope->isCurrent()) is false. So ContextObj::make_current() calls ContextObj::update(). ContextObj::update() calls CDOhash_map::save(). CDOhash_map::save() calls return new(pCMM) CDOhash_map(*this) which calls the copy constructor which reads the data using d_data(other.d_data). | |||
2015-10-23 | Switching Options::current() to return a pointer. This helps avoid undefined ↵ | Tim King | |
behavior due to dereferencing a null pointer in the future. | |||
2015-10-23 | This patch slightly generalizes how the std::isfinite function in <cmath> is ↵ | Tim King | |
referred. | |||
2015-10-22 | Enable counterexample-guided quantifier instantiation by default for ↵ | ajreynol | |
quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions. | |||
2015-10-21 | Minor refactoring in strings related to length. | ajreynol | |
2015-10-20 | Refactor strings, remove old cycle checks in normalize eqc. | ajreynol | |
2015-10-20 | Clean up explanations involving string length. Add regression. | ajreynol | |
2015-10-19 | Improve stratification of strings extended function reductions, add ↵ | ajreynol | |
regressions. Eliminate preprocess for regexp. | |||
2015-10-19 | Improve regexp rewriter, simplify regexp preprocess, add basic trans closure ↵ | ajreynol | |
for string contains, refactoring. | |||
2015-10-18 | Fix for no condense func values. | ajreynol | |
2015-10-16 | Add option to interleave enumerative instantiation with other strategies. | ajreynol | |
2015-10-16 | Throw error for recursively defined types involving Boolean. | ajreynol | |
2015-10-16 | Fix for codatatype constant rewrite, add regression. | ajreynol | |
2015-10-15 | Fix congruence check in strings, fixes bug 686. | ajreynol | |
2015-10-15 | Change semantics of str.substr to allow endpoint out of bounds, and return ↵ | ajreynol | |
empty string for error conditions. Improve rewriter for str.substr. | |||
2015-10-15 | Decompose string contains, minor refactoring. | ajreynol | |
2015-10-13 | remove options infrastructure code which depended on undefined behavior | Kshitij Bansal | |
appears to be source of crashes on mac | |||
2015-10-11 | fix regression tests, support fallback mode for proofs | Kshitij Bansal | |
2015-10-11 | Fix strings preprocessing + incremental, fixes bug 682. Add initial ↵ | ajreynol | |
infrastructure for str.contains inferences. | |||
2015-10-08 | Minor improvements to strings. Refactor rewriter. Enable fairness for ↵ | ajreynol | |
multiple sorts in UF finite model finding by default. | |||
2015-10-07 | Disabled donePPSimpITE when unsat-cores are enabled (fixes bug648) | Liana Hadarean | |
2015-10-07 | Minor improvements, add endpoint eq inference to strings. | ajreynol | |
2015-10-06 | More improvements to strings rewriter for regexps, contains, indexof, ↵ | ajreynol | |
replace and others. Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len. | |||
2015-10-02 | Fixes related to explanations for cycles, sym inferences. Minor fixes and ↵ | ajreynol | |
improvements. | |||
2015-10-02 | Improvements to rewriter for regexp, contains, indexof. Improvements and ↵ | ajreynol | |
fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions. | |||
2015-10-01 | Evaluate extended operators on partially concrete arguments. More aggressive ↵ | ajreynol | |
rewriting. Bug fix explanations for inferences. Avoid spurious cardinality splits. Do not do disequality splits for non-disequal terms. Work towards non-recursive handling of flat forms. | |||
2015-10-01 | More improvements to strings. More aggressive inference of constant eqc, ↵ | ajreynol | |
reductions based on congruence, precheck for cycles. | |||
2015-09-30 | Refactor strings, bug fix inferences vs lemmas. | ajreynol | |
2015-09-29 | Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add ↵ | ajreynol | |
regressions. | |||
2015-09-28 | Improve quantifiers engine wrt incremental presolve. Add regressions. | ajreynol | |
2015-09-28 | Minor fix | ajreynol | |
2015-09-28 | Minor fixes to strings, add regressions. | ajreynol | |
2015-09-28 | Fix bug for trivial extf inferences in strings. Improve caching for splits ↵ | ajreynol | |
in strings. Other improvements. | |||
2015-09-27 | Improved handling of extended operators. Do preprocess on memberships ↵ | ajreynol | |
eagerly, only process contains/memberships that have non-constant arguments. Cleanup. | |||
2015-09-26 | Lazy preprocessing of extended operators in strings. Add regressions. Fixes ↵ | ajreynol | |
bug 613. | |||
2015-09-26 | Better organization of quantifiers modules, promote full saturation to ↵ | ajreynol | |
module. Add heuristics for cbqi LIA instantiation with coefficients. | |||
2015-09-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ↵ | ajreynol | |
of term database, other refactoring. Bug fixes for cbqi+datatypes. | |||
2015-09-24 | Counterexample-guided instantiation for datatypes. Make sygus parsing more ↵ | ajreynol | |
liberal. | |||
2015-09-22 | Improve ITE redundant branch elimination in quantifiers. | ajreynol | |
2015-09-21 | Fix for sets segfault (reported by Ravi Kandhadai) | Kshitij Bansal | |
fix involves sets getModelValue handling the case when element theory doesn't have model | |||
2015-09-18 | Fix bug in quantifiers engine where model construction could be skipped. | ajreynol | |
2015-09-18 | More work mixing UF and sygus. | ajreynol | |
2015-09-18 | Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding ↵ | ajreynol | |
quantified formulas with non-constant polarity. | |||
2015-09-16 | Add option --fmf-fun-rlv, remove deprecated option --axiom-inst. | ajreynol | |
2015-09-15 | Fix bug related to quantifiers + incremental, thanks John Backes for the bug ↵ | ajreynol | |
report. Other minor cleanup. |