Age | Commit message (Collapse) | Author |
|
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.
|
|
|
|
discharged.
|
|
Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions.
Removing one test case from the integer regress0.
|
|
|
|
build issues
|
|
were not in the databas (queried by areEqual and areDisequal)
and it's a bit better
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3738&category=&p=-1&reference_id=3731
|
|
|
|
- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work.
- Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver.
- Fix to an assertion in CDQueue.
- Implements a CDArithVarSet using a vector of booleans and CDList.
- Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.
|
|
CDSet -> CDHashSet
|
|
still something fishy here, I think I need to merge in a few more things to support incrementality properly. But this fixes "make check" for now
|
|
function names and documentation.
|
|
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
|
|
will never be restored
|
|
upper bound.
|
|
* removed bvpicosat directory as it is currently not used
Cleared some of the flurry of warnings my previous merge caused in src/prop/
|
|
* theories that are parametric and therefore need the combination framwork should be tagged as "parametric" in the kinds file
* default care graph computation was not sufficient, fixed
|
|
|
|
This is a significant refactoring of code.
- r2820
-- Refactors Simplex so that it does significantly fewer functions.
-- Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model.
-- Some of the code for propagation has moved to TheoryArith.
-r2826
-- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound().
- r2827
-- Adds isZero() to Rational. Adds cmp to DeltaRational.
- r2831
-- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp.
-- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.
|
|
term is added.
|
|
|
|
CDO<size_t> into a FIFO queue.
|
|
traits---with the effect that everything with a kinds file is registered as a theory. Eventually we may want a more dynamic way of selecting theory implementations, but for now we don't have a need for this. Expected performance impact: none. (This commit addresses and re-closes the reopened bug #307.)
|
|
|
|
* separated SatSolverInput interface class into two classes:
- TheoryProxy for the sat solver to communicate with the theories
- SatSolverInterface abstract class to communicate with the sat solver
* instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
* added abstract classes for DPLLSatSolver and BVSatSolver different interfaces
Replaced TheoryBV with bitblasting implementation:
* all operators bitblasted
* only operator elimination rewrite rules so far
|
|
solve -> ppAsert
staticLearning -> ppStaticLearn
preprocess -> ppRewrite
SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*)
via Eclipse refactoring magic.
|
|
SMT-LIBv1 and SMT-LIBv2 input:
In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance:
(benchmark actually_a_sat_benchmark_but_looks_like_uf
:logic QF_UF
:cvc4_logic { QF_SAT }
[...]
In SMT-LIBv2, you use a set-info; for instance:
(set-logic QF_UF)
(set-info :cvc4-logic "QF_SAT")
[...]
Right now, the only thing this does is disable the symmetry breaker for
benchmarks like the above ones.
As part of this work, TheoryEngine::setLogic() was removed (the logic field there
wasn't actually used anywhere, its need disappeared when
Theory::setUninterpretedSortOwner() was provided).
Also, Theory::d_uninterpretedSortOwner got a name change to
Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory
class. This represents a breakage of our separation goals for CVC4, since it
means that two SmtEngines cannot be created separately to solve a QF_AX and
QF_UF problem. A bug report is pending.
|
|
(Clark-requested change)
|
|
|
|
to request a decision on a literal. All these theory requests are kept in a
context-dependent queue and serviced in order when the SAT solver goes to make a
decision. Requests that don't have a SAT literal give an assert-fail. Requests
for literals that already have an assignment are silently ignored.
Since the queue is CD, requests can actually be serviced more than once (e.g., if
a request is made at DL 5, but not serviced until DL 10, and later, a conflict
backtracks to level 7, the request may be serviced again).
Performance impact: none to negligible for theories that don't use it
See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0
|
|
|
|
(better, (marginally) faster -- regressions 3605, 3606)
|
|
platforms that need it; fixes Mac builds.
|
|
|
|
normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced.
Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
|
|
and other build/documentation fixes from yesterday's portfolio merge; resolves bug 302
|
|
my previous checkin)
|
|
|
|
|
|
(Though currently unused.)
For theories that request presolve and postsolve (in their kinds file),
they will get a presolve() notification before the first check(). After
the final check during the current search, they get a postsolve().
presolve() and postsolve() notifications always come in pairs, bracketing
all check()/propagate()/getValue() calls related to a single query. In
the case of incremental benchmarks, theories may get additional
presolve()/postsolve() pairs, but again, they always come in pairs.
Expected performance impact: none (for theories that don't use it)
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5
|
|
and SMT-LIBv2).
There are --enable-symmetry-breaker and --disable-symmetry-breaker
options that are always respected regardless of this default.
Expected performance impact: positive
New default (UF only) compared to old default (always on):
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5
Symmetry breaker remains a big win on UF:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5
The last link to results looks at first that the symmetry breaker should
always be turned off, since its use loses more regressions than it gains.
*However*, the lost ones are only our "QF_SAT" benchmarks. For these, we
should indeed turn off the symmetry breaker, but that's impossible for
now because we tag them internally with the logic "QF_UF."
|
|
manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.
|
|
r2650 to r2779.
- This excludes revision 2777. This revision had some strange performance implications and was delaying the merge.
- This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts.
- The DioSolver can be disabled at command line using --disable-dio-solver.
- This includes a number of changes to the arithmetic normal form.
- The Integer class features a number of new number theoretic function.
- This commit includes a few rather loud warning. I will do my best to take care of them today.
|