| Age | Commit message (Collapse) | Author |
|---|
|
after exhaustively enumerating finite types), also fix a standards-related FIXME in SmtEngine by clarifying the text of an error message
|
|
|
|
src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat.
The namespaces weren't changed, only the file locations.
|
|
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.
|
|
* change some uses of "std::cout" to "Message()"
* change some files to use Unix newlines instead of DOS newlines
* fix compiler warning
|
|
model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version
|
|
- new syntax for rewrite rules
- better rewrite rules theory
- remove the rewriting with rewrite rules during ppRewrite temporarily
- theory can define their own candidate generator
- define a general candidate generator (inefficient ask to every theory)
- split inst_match between the pattern matching used for quantifiers (inst_match.*) and
the one used for rewrite rules (rr_inst_match.*):
- the pattern matching is less exhaustive for quantifiers,
- the one for rewrite rules can use efficient-e-matching.
|
|
support yet for enumerating arrays, or for enumerating non-trivial datatypes.
|
|
(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
|
|
|
|
|
|
result
|
|
|
|
disabled in bitvectors due to non-stably infinite problems
the option to enable it is --theoryof-mode=term
|
|
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
|
|
|
|
* array now only propagates thropugh the equality engine
* assertions in the equality rewriting to ensure eq -> { eq, T, F }
|
|
|
|
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
|
|
Also fixed one bv rewrite failure (more to come)
|
|
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately
|
|
propagating disequalities between shared terms.
|
|
still doesnt fix the wrong answers thought :(
|
|
are still the AUFBV wrong results, but it seems better.
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
|
|
|
|
|
|
regressions. New additions:
* areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later.
* propagation of shared dis-equalities (not yet complete, once case missing)
* changes to the theories that use it, authors should check up on the changes
|
|
|
|
pushed out for relationships between terms tagged with the same tag. No performance impact.
|
|
- The type of (kind::DIVISION x y) is RealType.
- A reference to util/pseudoboolean.i was removed.
- rec5.cvc is disabled for now. The type of 2 is Integer which is not a subtype of [0..11].
|
|
This fixes bugs 335 and 333.
|
|
|
|
Added ITE simplifier - on by default only for QF_LIA benchmarks
Fixed one bug in arrays
Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()
|
|
* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations
|
|
Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor
|
|
arrays, fixed bug with equalities between constants in shared terms database
|
|
Also disabled eager lemmas - slows down QF_AX but gets new examples in QF_AUFBV
|
|
|
|
|
|
- This adds a CleanUp template argument to CDList.
- CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator.
- CDVector<T> has been simplified and improved.
- The expected performance impact is negligible.
|
|
Dump("foo") << FooCommand(...);
now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.
If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run. This is done even if the muzzle is on.
This commit also cleans up some code that used the dump feature (in arrays,
particularly).
|
|
CDSet -> CDHashSet
|
|
|
|
solve -> ppAsert
staticLearning -> ppStaticLearn
preprocess -> ppRewrite
SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*)
via Eclipse refactoring magic.
|
|
|
|
still write, for example:
#include "expr/node.h"
but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever),
have such #includes rewritten automatically to:
#include <cvc4/expr/node.h>
|
|
|
|
|
|
and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
|
|
|
