| Age | Commit message (Collapse) | Author |
|---|
|
|
|
infrastructure to BV collectModelInfo in preparation for bug fix.
|
|
* normalizing in bv before bitblasting
|
|
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
|
|
|
|
|
|
|
|
Minor fixes to bv and theory_engine
|
|
|
|
|
|
|
|
would require some graph coloring algorithm.
|
|
|
|
|
|
fix bug424
|
|
|
|
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.)
|
|
|
|
|
|
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables
|
|
documentation, etc.).
* Remove sat_module.cpp, which was no longer used (was previously refactored?)
|
|
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.
|
|
get bitblasted, it would restart to add the clauses, and loose propagation information.
|
|
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
|
|
* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally
|
|
IN_MODEL status
|
|
to TheoryEngine
|
|
|
