| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).
The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).
This is part of the ongoing effort to clean up the public interface.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
consistency, error-reporting, and documentation.
|
|
To enable, use --check-models. Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not. This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.
By default, --check-models is quiet (no output unless it detects a problem). That allows regression runs to pass unless there are problems:
make regress CVC4_REGRESSION_ARGS=--check-models
To see it work, use -v in addition to --check-models.
There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.
--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models. This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).
Also:
* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
|
|
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
|
|
documentation, etc.).
* Remove sat_module.cpp, which was no longer used (was previously refactored?)
|
|
|
|
isConst() and isVar() as appropriate)
also some base infrastructure for the new ::isConst().
|
|
1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)
The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:
* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important. If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***
Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).
Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double). For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).
Benefits of the new options system include:
1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose
I've taken lots of care not to break anything. Hopefully, I've succeeded in that.
|
|
See below for details.
* Fix the "assert" name-collision bug (resolves bug #364).
Our identifiers should never be named "assert", as that's a preprocessor
definition in <assert.h>, which is often #included indirectly (so simply
having a policy of not including <assert.h> isn't good enough---one of
our dependences might include it). It was once the case that we didn't
have anything named "assert", but "assert()" has now crept back in.
Instead, name things "assertFoo()" or similar. Thanks to Tim for the
report.
To fix this, I've changed some of Dejan's circuit-propagator code from
"assert()" to "assertTrue()". Ditto for Andy's explanation manager.
Guys, if you prefer a different name in your code, please change it.
* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
Inner lets now shadow outer lets (previously, they incorrectly gave an
error). Additionally, while looking at this, I found that a sequential let
was implemented rather than a parallel let. This is now fixed. Thanks to
Liana for the report.
* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).
* There were a lot of Debug lines in bitvectors that had embedded toString()
calls. This wasted a LOT of time in debug builds for BV benchmarks
(like in "make regress"). Added if(Debug.isOn(...)) guards; much faster
now.
* Support for building public-facing interface documentation only (as opposed
to all internals documentation). Now "make doc" does the public-facing and
"make doc-internals" does documentation of everything. (Along with changes
to the nightly build script---which will now build and publish both types
of Doxygen documentation---this resolves bug #359).
* Fix the lambda typechecking bug (resolves bug #322). Thanks to Andy for the
report (a long long time ago--sorry).
* The default output language for all streams is now based on the current set
of Options (if there is one). This has been a constant annoyance, especially
when stringstreams are used to construct output. However, it doesn't work
for calls from outside the library, so it's mainly an annoyance-fixer for
CVC4 library code itself.
* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
are used only in assertions-enabled builds (and thus give warnings in
production builds). This was briefly discussed at the meeting this week.
|
|
\file tags corrected, copyright added to files that had it missing, etc.
I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
|
|
|
