| Age | Commit message (Collapse) | Author |
|---|
|
In SmtEngine::setDefaults() we were setting options such as
--simplifciation=none for unsat cores but not proofs. Producing unsat
cores relies on the same infrastructure as proofs and should be a subset
of the same work in most cases. Thus, this commit changes
SmtEngine::setDefaults() to set the same options for proofs as we
previously only did for unsat cores. Additionally, it changes the
function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH
if proofs and unsat cores are not enabled. Fixes issue #1953.
|
|
This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation.
The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick.
This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.
|
|
Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).
This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.
|
|
|
|
sygus), update regressions.
|
|
|
|
|
|
|
|
|
|
|
|
commit for nlAlgMaster.
|
|
|
|
With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.
|
|
Morgan's proof branch).
|
|
types get sent to the theory of the type.
Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.
|
|
|
|
|
|
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
|
|
|
|
|
|
-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.
- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.
- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.
Minor Changes:
- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.
- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
|
|
success, nonzero error
|
|
|
|
|
|
allows linearization of div,mod,/ by a constant.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
arithmetic.
|
|
DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
|
|
multiplication.
|
|
for division by 0.
|
|
discovered (still outstanding). :-(
* Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night)
* Provide expected output for arith regression 'mod.01.smt2'
* Also, fix a compiler warning in inst_gen.cpp
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
should work now
|
|
reenqueued so that the queue was a superset of the failing assertions. This adds a super expensive debug routine unenqueuedVariablesAreConsistent() that catches this bug. This is enabled when -d arith::consistency is turned on. make check passes with this flag enabled.
|
|
|
|
(no performace or search behavior changes expected)
|
|
|
|
|
|
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.
|
|
back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"
|
|
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.
|
|
|
