summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Collapse)Author
2014-03-04Guard java-specific swig code with SWIGJAVA.Thomas Hunger
Without this building just the python bindings will fail. Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-02-28a new regular expression engine for solving both positive and negative ↵Tianyi Liang
membership constraints
2014-02-21portfolio: fix export of emptysetKshitij Bansal
2014-02-20Fix ite and iff handling in QCF. Add option for heuristic instantiation in ↵Andrew Reynolds
QCF (not working yet). Improve automatic option setting for quantifiers.
2014-02-18switch to total function str.to.int: maps invalid and non-digit strings to 0Tianyi Liang
2014-02-17bring back the commits which is lost accidentally.Tianyi Liang
2014-02-17add str2intTianyi Liang
2014-02-17Fix for strings-exp: enable quantifiersMorgan Deters
2014-02-17Fix strings preprocessing for justification heuristicMorgan Deters
2014-02-17type conversionTianyi Liang
2014-02-13fix expanding defTianyi Liang
2014-01-28merge internal and user of charat & substr into oneTianyi Liang
2014-01-22Some minor fixes to SmtEngine strings settings.Morgan Deters
2014-01-22add warning for using strings in ALL_SUPPORTEDTianyi Liang
2014-01-22Smarter options, but still have a bugTianyi Liang
2014-01-18strings with new ideasTianyi Liang
2014-01-16adds partial functionsTianyi Liang
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified ↵Andrew Reynolds
formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
2014-01-03Removing and consolidating options for uf-ss and quantifiers. Bug fix for ↵Andrew Reynolds
inst gen-style MBQI.
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing ↵Andrew Reynolds
proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.
2013-12-24Java datatype API fixups, datatype API examplesMorgan 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-16First attempt at incorporating LFSC proof checker into CVC4.Morgan Deters
2013-12-16Fix for bug 544.Morgan Deters
2013-12-10Whitespace.Morgan Deters
2013-12-10Remove "NodeValue width" outputMorgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback