Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters | |
2013-12-16 | Fix for bug 544. | Morgan Deters | |
2013-12-13 | Fix link error when using clang. | Morgan Deters | |
2013-12-10 | Fix timer statistics to report correct time even on process abort. | Morgan Deters | |
2013-12-10 | Whitespace. | Morgan Deters | |
2013-12-10 | Fix warning. | Morgan Deters | |
2013-12-10 | Remove "NodeValue width" output | Morgan Deters | |
2013-12-07 | fix bug 542 | Kshitij Bansal | |
2013-12-05 | disable substring in default mode | Tianyi Liang | |
2013-12-05 | Fix NodeValue bitfields for 32-bit; fix comment. | Morgan Deters | |
2013-12-05 | Minor cleanup. | Morgan Deters | |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters | |
2013-12-05 | Fixes related to parametric datatype printing. | Morgan Deters | |
2013-12-05 | Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now ↵ | Morgan Deters | |
works). | |||
2013-12-04 | Minor cleanup. | Morgan Deters | |
2013-12-04 | Partial kind branch merge, including new --rewrite-apply-to-const feature. | Morgan Deters | |
2013-12-04 | Don't put define-funs in model output; bug 411 testcase no longer relevant. | Morgan Deters | |
2013-12-04 | More Java bindings fixes | Morgan Deters | |
2013-12-03 | adds LB strategy | Tianyi Liang | |
2013-12-03 | Some fixes for swig warnings. | Morgan Deters | |
2013-12-03 | Last version for undelayed LB | Tianyi Liang | |
2013-12-03 | Work around a swig segfault issue when building on Mac OS | Morgan Deters | |
2013-12-03 | string fmf perfomance fix | Tianyi Liang | |
2013-12-03 | string fmf changes | Tianyi Liang | |
2013-12-02 | SExpr pretty-printing for :all-options and :all-statistics. | Morgan Deters | |
2013-12-02 | Minor cleanup. | Morgan Deters | |
2013-12-02 | Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a ↵ | Morgan Deters | |
subtype of (Pair Real Real). Resolves bug #541. | |||
2013-12-02 | fixed rewriter bug where postRewrite was not caching properly | lianah | |
2013-12-02 | Another fix to Java destruction order issues. Thanks to Zheng Manchun for ↵ | Morgan Deters | |
the report. | |||
2013-11-29 | Fix proofs build. | Morgan Deters | |
2013-11-29 | Fix portfolio compile error. | Morgan Deters | |
2013-11-27 | Fix for compile error when using gcc 4.7 with -std=gnu++11. Thanks to ↵ | Morgan Deters | |
Martin Brain for the patch! | |||
2013-11-27 | General pre-release cleanup commit | Morgan Deters | |
* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing | |||
2013-11-27 | Java bindings improvements for CASCADE, minor cleanup. | Morgan Deters | |
2013-11-27 | Add missing template instanatiation in Java bindings | Morgan Deters | |
2013-11-27 | Incremental is now on by default when using from API, off for command-line ↵ | Morgan Deters | |
driver except in interactive mode. | |||
2013-11-26 | Bug fix for E-matching select terms, minor fix for bounded integers, bug fix ↵ | Andrew Reynolds | |
to improve performance of quantifiers rewriter | |||
2013-11-26 | Fix a segfault in the printer infrastructure when called from API and no ↵ | Morgan Deters | |
language is set | |||
2013-11-26 | Fix C++-to-Java exception translation. | Morgan Deters | |
2013-11-26 | Fix Java output stream adapter. | Morgan Deters | |
2013-11-26 | Fix Java destruction order issue; thanks to Zheng Manchun for reporting this ↵ | Morgan Deters | |
bug. | |||
2013-11-26 | Minor fix for swig bindings. | Morgan Deters | |
2013-11-25 | Merge remote-tracking branch 'CVC4root/master' | Tim King | |
2013-11-25 | Substantial Changes: | Tim King | |
-ITE Simplification -- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities. -- Separated simpWithCare from simpITE. -- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants. -- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically. -- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks. -- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches. - TheoryEngine -- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above. -- Switched UnconstrainedSimplifier to a pointer. - RemoveITEs -- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. - Theory Bool Rewriter -- Added additional simplifications for boolean ites. Minor Changes: - TheoryModel -- Removed vestigial copy of the ITESimplifier. - AttributeManager -- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. -NodeManager -- Added additional functions for reclaiming zombies. -- Exposed the size of the node pool for heuristics that worry about memory consumption. - NaryBuilder -- Added convenience classes for constructing associative and commutative n-ary operators. -- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.) | |||
2013-11-25 | Array collectModelInfo fix for Andy | Clark Barrett | |
2013-11-21 | Adding the changes needed to delete rewriter attributes. This includes ↵ | Tim King | |
being able to list attributes. Additionally, added debugging hooks to node manager and attribute manager. | |||
2013-11-20 | Changing the number of bits allocated per field in node values. | Tim King | |
2013-11-19 | Bug fix for previous commit | Andrew Reynolds | |
2013-11-19 | Add fair strategy for finite model finding multiple sorts --uf-ss-fair. | Andrew Reynolds | |
2013-11-14 | Allow empty record literals (fixing an oversight in previous work on empty ↵ | Morgan Deters | |
tuples/records) |