summaryrefslogtreecommitdiff
path: root/src/prop
AgeCommit message (Collapse)Author
2014-05-20Fix compiler warning (missing virtual dtor)Morgan Deters
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-03-19Appease compilers from latest XCode release (v5.1).Morgan Deters
2014-03-11Merge branch '1.3.x'Morgan Deters
2014-03-11Fix for rewriterules build breakage.Morgan Deters
2014-03-11Fix for random-seed option.Morgan Deters
2014-03-11Merge branch '1.3.x'Morgan Deters
2014-03-11Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.Morgan Deters
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵Morgan Deters
(resolves bug #548).
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-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27Fix for compile error when using gcc 4.7 with -std=gnu++11. Thanks to ↵Morgan Deters
Martin Brain for the patch!
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-10-09fixed uf proof bug: now storing deleted theory lemmaslianah
2013-10-08fixed uf proof with holes bugslianah
2013-10-07fixed some bugsLiana Hadarean
2013-10-07first draft implementation of uf proofs with holesLiana Hadarean
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-06-25Proposed fix for bug #513Morgan Deters
2013-05-10now proofs print mapping between atom and propositional variable as a ↵lianah
comment in LFSC
2013-05-10fixes to the proof system so it works with theory lemmas and explanationslianah
2013-05-08rm decision/relevancyKshitij Bansal
2013-05-07fix for nonterminating model-based array loopMorgan Deters
2013-04-30added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ↵lianah
ExtractSignExtend) and bvurem lemma
2013-04-30added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-30added support for dumping the SAT problem the sat solver is working onlianah
2013-04-26Merge experimental decisionweight branchKshitij Bansal
None of these are enabled by default, so any performance impact counts as a bug Options added are: --decision-threshold=N :default 0 + ignore all nodes greater than threshold in first attempt to pick decision --decision-use-weight bool :default false + use the weight nodes (locally, by looking at children) to direct recursive search --decision-random-weight=N int :default 0 + assign random weights to nodes between 0 and N-1 (0: disable) --decision-weight-internal=HOW + computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) Squashed commit of the following: commit 0dbae066c19abde37092517b50f23255398539db Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Fri Apr 26 16:42:36 2013 -0400 contentless cleanup commit 62bb99b33deceb803ba5afc563fd322b4b5d1b7e Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Tue Apr 16 21:43:55 2013 -0400 bugfixes in usr1 auto weight computation commit 9f039cba805bfd722466734920e758d48ae3b23e Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Fri Mar 29 15:01:33 2013 -0400 DECISION_WEIGHT_INTERNAL_USR1 commit 744e16d514594e5f1c69b36473b03cf501d9b9d1 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Wed Mar 27 11:05:43 2013 -0400 split theory and decision requests commit f379d8a821df31c74b42a7722e891abc5c944f16 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Wed Mar 27 09:51:58 2013 -0400 fix potential bug with threshold commit 3dcb45eb5ee648d3edbeddf76b838076afea3d12 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Wed Feb 27 20:29:38 2013 -0500 stat bv::weightComputationTimer commit 2ab97d063e221357d2bb017af4589105777fd5a3 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Sat Feb 23 17:02:43 2013 -0500 decision: option to auto compute weight of boolean structure commit 0a8c29e699ad96d5f73bc14d31ad9254f6711ae8 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Sat Feb 23 14:53:50 2013 -0500 decision: fix design to do partial explorations * make findSplitterRec and all related helper functions' return type trivalued, to be able to distinguish between "partial exploration" vs "done exploration but found nothing" * keep additional data structure to remember to what extent the partial exploration has been completed so not to repeat it. we can use this to make multiple passes on formula with arbritrary order of thresholds for exploration commit 0815991fc1b0f1d63f0e8124d4672d782e89d671 Author: lianah <lianahady@gmail.com> Date: Fri Feb 22 17:55:40 2013 -0500 added simple node weight computation for bv. commit e4c507e2e2fdc8794fd04c31093660a80c7f44c3 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Wed Feb 20 02:35:21 2013 -0500 --decision-use-weight, --decision-random-weight=N commit 0624177d66d6ed2b3cc7fdb13df775990cfe50c2 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Tue Feb 19 23:36:49 2013 -0500 decisionThreshold option commit ac3579a52e452e3118ce116ff1823d6c6885544b Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Tue Feb 19 20:22:51 2013 -0500 DecisionWeightAttr
2013-04-03* changing the bitblast-eager to bitblast on pre-registerDejan Jovanović
* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate) * when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true) * bitblast-eager implies decision=internal
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-29removing cryptominisat since we're not using itDejan Jovanović
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds ↵Morgan Deters
and src
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
* build bugfix for win32 * also fix a bug re: tuples and records in the datatypes rewriter These fixes are for both trunk and 1.0.x branches. (cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
* build bugfix for win32 * also fix a bug re: tuples and records in the datatypes rewriter These fixes are for both trunk and 1.0.x branches.
2012-12-05This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ↵Tim King
CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.
2012-11-26fixup for incremental solvingDejan Jovanović
2012-11-14fix a race problem. due to interrupt mechanism minisat returned true instead ↵Kshitij Bansal
of undef.
2012-10-24fix for bug 429 Dejan Jovanović
* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09* Add assertion in TheoryModel code to ensure we don't get inconsistentMorgan Deters
substitutions for solved variables. Related to bug 418 (and might resolve it). * Respect phase-locking in Minisat (one phase-saving site was unguarded). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-06* Clean up some options documentationMorgan Deters
* Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-05Bug-related:Morgan Deters
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-03added support for interrupting TheoryBVLiana Hadarean
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to ↵Morgan Deters
make it unambiguous for case-insensitive filesystems like on Mac. Fixes Mac builds
2012-09-28Public interface review items:Morgan Deters
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument() * Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only * CheckArgument() throws non-AssertionException * things outside the core library (parsers, driver) use regular C-style assert, or a public exception type. * auto-generated documentation for Smt options and internal options Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback