Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(resolves bug #548).
|
|
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
|
|
|
|
Martin Brain for the patch!
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
comment in LFSC
|
|
|
|
|
|
|
|
ExtractSignExtend) and bvurem lemma
|
|
|
|
|
|
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
|
|
* 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
|
|
|
|
|
|
|
|
|
|
and src
|
|
* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles
|
|
|
|
* 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)
|
|
* 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.
|
|
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.
|
|
|
|
of undef.
|
|
* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue
|
|
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.)
|
|
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.)
|
|
* 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.)
|
|
* 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
|
|
|
|
|
|
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables
|
|
make it unambiguous for case-insensitive filesystems like on Mac. Fixes Mac builds
|
|
* 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.
|