summaryrefslogtreecommitdiff
path: root/src/util
AgeCommit message (Collapse)Author
2014-01-09add constant replace, indexofTianyi Liang
2014-01-02Merge branch '1.3.x'Morgan Deters
2014-01-02Update copyright year.Morgan Deters
2013-12-26new functions in stringsTianyi Liang
2013-12-25fix for some nightly build failuresMorgan Deters
2013-12-24Merge branch '1.3.x'Morgan Deters
Conflicts: NEWS
2013-12-24Minor code cleanup.Morgan Deters
2013-12-24Java datatype API fixups, datatype API examplesMorgan Deters
2013-12-17some config changes: new --bsd option, readline gives warning, default build ↵Morgan Deters
is now production.
2013-12-13Fix link error when using clang.Morgan Deters
2013-12-10Fix timer statistics to report correct time even on process abort.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-04More Java bindings fixesMorgan Deters
2013-12-03Some fixes for swig warnings.Morgan Deters
2013-12-03Work around a swig segfault issue when building on Mac OSMorgan Deters
2013-11-27General pre-release cleanup commitMorgan 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-27Java bindings improvements for CASCADE, minor cleanup.Morgan Deters
2013-11-25Substantial 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-14Datatype::getCardinality() cachingMorgan Deters
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-10-23bug fixTianyi Liang
2013-10-21remove nested re or; opt loopTianyi Liang
2013-10-20adds regular expression rangeTianyi Liang
2013-10-11add constant membershipTianyi Liang
2013-10-11adds native regexp.Tianyi Liang
2013-10-08Optimizations for datatypes theory. There seems to be a bug in ↵Andrew Reynolds
trans_closure, currently implemented a work around.
2013-10-03Added support for converting unsorted problems to multi-sorted problems via ↵Andrew Reynolds
sort inference and monotonicity. Minor cleanup.
2013-09-30Bug fixes and improvements for symmetry breaking, it now supports multiple ↵Andrew Reynolds
sorts. Working on monotonicity inference.
2013-09-27Merge branch 'master' of github.com:tiliang/CVC4Morgan Deters
2013-09-27Add new symmetry breaking technique for finite model finding. Improvements ↵Andrew Reynolds
to bounded integer quantifier instantiation.
2013-09-27adds model generation for strings, and a hacked way in arith engine for modelsTianyi Liang
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-11Theory of strings.Tianyi Liang
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-09-09Support empty (and 1-ary) tuples and records.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-13Remove now-unused language bindings interface file.Morgan Deters
2013-07-13Fix language bindings and portfolio builds.Morgan Deters
2013-07-12Fix for curious GCC 4.8 translation with -O.Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
2013-07-06Model output is now const; this related to bug 519Morgan Deters
2013-06-27Remove output.h from public space, to avoid clashes with symbols defined in ↵Morgan Deters
users' space. Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's not installed on users' machines, and public headers should not include it. Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-27Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they ↵Morgan Deters
don't escape to user space Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-24Add files missing from last commitMorgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵Morgan Deters
allows linearization of div,mod,/ by a constant.
2013-06-24Add options for symmetry breaking in uf+ss totality axiom approach, option ↵Andrew Reynolds
for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
2013-05-21Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵Morgan Deters
to improper ITE removal in quantifier instantiations.
2013-04-26FCSimplex branch mergeTim King
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback