| Age | Commit message (Collapse) | Author |
|---|
|
builds, an Unhandled(SExpr::SexprTypes) could not compile on debian.
|
|
|
|
* 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)
|
|
* 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.
|
|
|
|
The available SAT solvers can be seen with the --show-sat-solvers option.
|
|
TheoryArith. This had been disabled for several months.
|
|
* 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).
|
|
build issues
|
|
CDSet -> CDHashSet
|
|
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!
|
|
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.
|
|
* 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
|
|
|
|
platforms that need it; fixes Mac builds.
|
|
and other build/documentation fixes from yesterday's portfolio merge; resolves bug 302
|
|
|
|
|
|
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.
|
|
|
|
|
|
* with a patched SWIG, the ocaml bindings build correctly.
** I will provide my patch to the SWIG dev team.
* fixed some class interfaces to play more nicely with SWIG.
* php, perl, tcl now work; examples added.
* improved binding module building and installation.
Also:
Stop #defining NULL ((void*) 0). This has been in cvc4_public.h for
a long, long time, I forget why I added it in the first place, and
it's a very, very bad idea. In C++, certain things are permitted
for NULL that aren't permitted for ((void*) 0), like for instance
implicit conversion to any pointer type. We didn't see an issue
here (until now, when interfacing with SWIG), because GCC is usually
pretty smart at working around such a broken #definition of NULL.
But that's fragile.
New exception-free Command architecture. Previously, some command
invocations were wrapped in a try {} catch() {} and printed out an
error. This is much more consistent now. Each Command invocation
results in a CommandStatus. The status can be "unsupported",
"error", or "success" (these are each derived classes, though, not
strings, so that they can be easily printed in a language-specific
way... e.g., in SMT-LIBv2, they are printed in a manner consistent
with the spec, and "success" is not printed if the print-success
option is off.) All Command functionality are now no-throw
functions, which @cconway reports is a Good Thing for Google
(where all C++ exceptions are suspect), and also I think is much
cleaner than the old way in this instance.
Added an --smtlib2 option that enables an "SMT-LIBv2 compliance
mode"---really it just sets a few other options like strictParsing,
inputLanguage, and printSuccess. In the future we might put other
options into a compliance mode, or we might choose to make it the
default.
|
|
Datatypes (bug #283) by Chris Conway. Thanks, Chris!
|
|
|
|
|
|
|
|
|
|
|
|
errors; reduces clutter, increases usability
|
|
|
|
/ long
|
|
|
|
getUnsignedLong().
|
|
SmtEngine::getProof(), a few other things..
|
|
Nodes---useful for debugging.
* language-dependent Node::toString()
* some minor proof-related cleanup
|
|
- can now output LFSC checkable resolution proofs
- added configuration option --enable-proof
- added command line argument --proof
To turn proofs on build with proofs enabled and run with --proof.
|
|
|
|
* OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want).
* Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch.
* --limit / --time-limit options renamed --rlimit and --tlimit.
There may be slowdown from disabling pseudobooleans.
|
|
v4.5.1 which has a buggy optimizer (resolves bug #266)
|
|
|
|
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
|
|
the dev mailing list.
|
|
|
|
|
|
|
