Age | Commit message (Collapse) | Author | |
---|---|---|---|
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) | |||
2013-11-14 | Datatype::getCardinality() caching | Morgan Deters | |
2013-11-13 | Add virtual destructors where missing | Morgan Deters | |
2013-11-13 | Some patches to CVC3 compatibility layer; Thanks to Adam Buchbinder @ Google ↵ | Morgan Deters | |
for the report and patch! | |||
2013-11-12 | Minor portfolio fixes for some platforms. | Morgan Deters | |
2013-11-12 | lb change | Tianyi Liang | |
2013-11-12 | add string progress measurements | Tianyi Liang | |
2013-11-12 | add loop cache | Tianyi Liang | |
2013-11-12 | Minor build system cleanup | Morgan Deters | |
2013-11-11 | length lemma is changed, var-split lemma is changed | Tianyi Liang | |
2013-11-11 | Expanded usefulness of (set-info :cvc4-logic ...) | Morgan Deters | |
2013-11-11 | Some fixes to build system with dependency-tracking is off; should fix ↵ | Morgan Deters | |
RPM/Debian builds. | |||
2013-11-11 | Change exit status to be more consistent with other command-line tools: 0 ↵ | Morgan Deters | |
success, nonzero error | |||
2013-11-10 | Fix compat-java library naming on Mac OS; thanks to Zheng Manchun for ↵ | Morgan Deters | |
reporting this issue | |||
2013-11-08 | Fix "make distclean", which should fix some of the build issues from last night | Morgan Deters | |