summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2013-12-26new functions in stringsTianyi Liang
2013-12-24Merge branch '1.3.x'Morgan Deters
Conflicts: NEWS
2013-12-24Minor code cleanup.Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof ↵Morgan Deters
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-12-05disable substring in default modeTianyi Liang
2013-12-05Minor cleanup.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-03adds LB strategyTianyi Liang
2013-12-03Some fixes for swig warnings.Morgan Deters
2013-12-03Last version for undelayed LBTianyi Liang
2013-12-03string fmf perfomance fixTianyi Liang
2013-12-03string fmf changesTianyi Liang
2013-12-02fixed rewriter bug where postRewrite was not caching properlylianah
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-26Bug fix for E-matching select terms, minor fix for bounded integers, bug fix ↵Andrew Reynolds
to improve performance of quantifiers rewriter
2013-11-25Merge remote-tracking branch 'CVC4root/master'Tim King
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-25Array collectModelInfo fix for AndyClark Barrett
2013-11-21Adding 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-19Bug fix for previous commitAndrew Reynolds
2013-11-19Add fair strategy for finite model finding multiple sorts --uf-ss-fair.Andrew Reynolds
2013-11-14Allow empty record literals (fixing an oversight in previous work on empty ↵Morgan Deters
tuples/records)
2013-11-12lb changeTianyi Liang
2013-11-12add string progress measurementsTianyi Liang
2013-11-12add loop cacheTianyi Liang
2013-11-11length lemma is changed, var-split lemma is changedTianyi Liang
2013-11-11Some fixes to build system with dependency-tracking is off; should fix ↵Morgan Deters
RPM/Debian builds.
2013-11-07Minor fixups to last commitMorgan Deters
2013-11-07Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-11-07Adds the header file into makefile, solving building error; adds cache for ↵Tianyi Liang
derivative; disables loop detection when finite model finding is enabled.
2013-11-06bug fixTianyi Liang
2013-11-06change optionsTianyi Liang
2013-11-06Bug fixes for bounded integer quantification. Current best strategy is to ↵Andrew Reynolds
turn off MBQI. Disable relevant triggers by default.
2013-11-06add seperate regular expression filesTianyi Liang
2013-11-04Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-10-24Fix for bug515Clark Barrett
2013-10-23add back eager approachTianyi Liang
2013-10-23bug fix for loop ruleTianyi Liang
2013-10-23bug fixTianyi Liang
2013-10-22bug fixes: some issues remain, need more discussion laterTianyi Liang
2013-10-21remove nested re or; opt loopTianyi Liang
2013-10-21string fixTianyi Liang
2013-10-21bug fix for string special caseTianyi Liang
2013-10-20adds regular expression rangeTianyi Liang
2013-10-16adds fmf for stringsTianyi Liang
2013-10-16renames for strings fmfTianyi Liang
2013-10-15bug fix in strings : change from assert to alwaysassertTianyi Liang
2013-10-15removes some junksTianyi Liang
2013-10-15performance optimizations for quantifier instantiationAndrew Reynolds
2013-10-15bug fix: string cache cleaningTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback