| 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.
|
|
enabled; and to makefile standards conformance
|
|
|
|
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
|
|
explicitly linked in with -l) when using CLN. Fixes a bug on recent Debian that Francois reported. Hopefully this doesn't break anything..
|
|
|
|
- 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)
|
|
|
|
errors; threading support should only be required to build pcvc4, not cvc4
|
|
|
|
configure time; fixes a bug reported by Clark for static-binary builds on machines where no static libreadline is available (like CIMS machines)
|
|
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)
|
|
library an error; useful for builds requiring a "pcvc4" binary at the end
|
