summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Collapse)Author
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-05Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now ↵Morgan Deters
works).
2013-12-04Partial kind branch merge, including new --rewrite-apply-to-const feature.Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
2013-12-02Another fix to Java destruction order issues. Thanks to Zheng Manchun for ↵Morgan Deters
the report.
2013-11-29Fix proofs build.Morgan 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-27Incremental is now on by default when using from API, off for command-line ↵Morgan Deters
driver except in interactive mode.
2013-11-26Fix Java destruction order issue; thanks to Zheng Manchun for reporting this ↵Morgan Deters
bug.
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-20Changing the number of bits allocated per field in node values.Tim King
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-11-05fixed proof regression script and added a new uf test caselianah
2013-11-04Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-10-28Turn off model-based arrays (causing crashes in portfolio)Clark Barrett
2013-10-09fixed options::proof() segfaultlianah
2013-10-09cleaned up proof codelianah
2013-10-09fixed uf proof bug: now storing deleted theory lemmaslianah
2013-10-09More improvements to datatypes, eager selector collapsing, improved collect ↵Andrew Reynolds
model info. Also fix bug in model post-processor.
2013-10-08added currying for uf proofs; still needs debugginglianah
2013-10-07Multiple fixes for datatypes theory solver: add support for parametric ↵Andrew Reynolds
datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
2013-10-03Added support for converting unsorted problems to multi-sorted problems via ↵Andrew Reynolds
sort inference and monotonicity. Minor cleanup.
2013-09-30replace with a new method for disequality, move to QF_STianyi Liang
2013-09-27Some fixes to recent strings commits.Morgan Deters
2013-09-27Merge branch 'master' of github.com:tiliang/CVC4Morgan Deters
2013-09-27adds communication with arith engineTianyi Liang
2013-09-27Add new symmetry breaking technique for finite model finding. Improvements ↵Andrew Reynolds
to bounded integer quantifier instantiation.
2013-09-27removes unsound cases, adds unrollingTianyi Liang
2013-09-24Better fix for bug 528Clark Barrett
2013-09-23Revert Clark's last commit, at his request; there are some bugs.Morgan Deters
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
2013-09-23Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.hClark Barrett
for faster compilation
2013-09-19Fix for bug 528Clark Barrett
2013-09-18Fixes to theoryof-mode; no longer static in Theory class.Morgan Deters
2013-09-16Fix (extraneous) command dumping.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-09Fix declare-datatypes dumping bug (bug 385).Morgan Deters
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a ↵Morgan Deters
segfault in smt2 printer
2013-08-20Change recursive expandDefinitions() to an interative worklist-based one; we ↵Morgan Deters
were blowing the stack. Fixes a segfault reported by Pantazis Deligiannis.
2013-08-08Fix a serious bug in the preprocessor; problem inputs reported by Pantazis ↵Morgan Deters
Deligiannis.
2013-08-08Parameterized, uninterpreted sorts need no Boolean-term conversionMorgan Deters
2013-07-24Regressions now checking models on unknown too. But quantifiers don't have ↵Morgan Deters
to be simplified by check-model in that case.
2013-07-24Don't allow --stats if not a statistics-enabled buildMorgan Deters
2013-07-23(get-info :all-options) to get option values; also command-line option ↵Morgan Deters
suggestions
2013-07-17Fix bug 516; include some bug testcases.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-11Fix for Boolean-term rewriting and LAMBDAsMorgan Deters
2013-07-06Model output is now const; this related to bug 519Morgan Deters
2013-06-25Merge branch '1.2.x'Morgan 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback