| Age | Commit message (Collapse) | Author |
|---|
|
Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.
Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin
|
|
Below is a highlight of the changes:
- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
Roughly speaking this means: (= x (+ y z)) is in normal form.
(See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.
|
|
|
|
headers.
|
|
|
|
builds, an Unhandled(SExpr::SexprTypes) could not compile on debian.
|
|
|
|
* Fix DefineFunctionCommand when a constant is defined
|
|
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)
|
|
Makefile.am files under src/prop/cryptominisat.
|
|
|
|
back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"
|
|
|
|
cc_min=2 in solve
|
|
|
|
* modified BVMinisat to work incrementally
* added more bv regressions
|
|
|
|
|
|
- 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.
|
|
|
|
|
|
|
|
|
|
pointers cannot be directly used with the CVC4_THREADLOCAL macro. This is why there were problems on macs.
|
|
|
|
|
|
(it wasn't used)
|
|
|
|
REWRITE_AGAIN calls.
|
|
|
|
|
|
|
|
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3828&category=&p=5&reference_id=3820
|
|
The available SAT solvers can be seen with the --show-sat-solvers option.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
TheoryArith. This had been disabled for several months.
|
|
* some sharing improvements based on model
|
|
* added simplification rewrites
|
|
|
|
(Can be overridden with --simplification=batch, for example.)
|
|
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).
|
|
to an out-of-place parenthesis
|
|
unintentionally allowing a theory to propagate p and ~p at the same time (and the conflict was undetected, leading to an incorrect answer). Credit to Clark for finding this.
|
