| Age | Commit message (Collapse) | Author |
|---|
|
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
|
|
|
|
By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.
If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.
|
|
SmtEngine resolved.
ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.
|
|
are still the AUFBV wrong results, but it seems better.
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
|
|
|
|
QF_UF and maybe others
|
|
|
|
the branch arithmetic/remove_const_int.
|
|
|
|
* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations
|
|
This should also fix bug 325.
|
|
Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor
|
|
src/theory/logic_info.{h,cpp} contains the CVC4::LogicInfo class, which keeps
track of which theories are active (which should remain constant throughout
the life of an SmtEngine) and other details (like integers, reals,
linear/nonlinear, etc.).
This class has a default constructor which is the most all-inclusive logic.
Alternatively, this class can be constructed from an SMT-LIB logic string
(the empty string gives the same as "QF_SAT"). Once constructed, theories
can be enabled or disabled, quantifiers flipped on and off, integers flipped
on and off, etc. At any point an SMT-LIB-like logic string can be extracted.
The SmtEngine keeps a LogicInfo for itself and shares with the TheoryEngine
(and, in turn, the theories) only a const reference to it. This ensures that
the logic info doesn't mutate over the course of the run.
As part of this commit, the TheoryEngine's old notion of "active theories"
has been completely removed. As a result, SMT benchmarks that are incorrectly
tagged with a logic will assert-fail or worse. (We should probably fail
more gracefully in this case.) One such example was bug303.smt2,
which used UF reasoning but was tagged QF_LIA. This has been fixed.
|
|
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.
|
|
|
|
- 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.
|
|
|
|
|
|
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.
|
|
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!
|
|
* 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
|
|
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
|
|
assertions off.
|
|
|
|
Datatypes (bug #283) by Chris Conway. Thanks, Chris!
|
|
|
|
subtle linker change in Ubuntu 11.10 oneiric :-(
|
|
* 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.
|
|
|
|
|
|
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.
|
|
to model gen on booleans; and a little cleanup
|
|
and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
|
|
|
|
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
|
|
|
|
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
|
|
|
|
minor fix-ups to documentation and some node stuff
|
|
|
|
constructor nodes created internally are given a type ascription
|
|
branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
(where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF
|
|
simplifications for the "muzzled" (i.e. competition) design, which had
been broken. Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like
Warning() << expensiveFunction();
Also, fix some compiler warnings.
|
|
|
|
|
|
* new "well-foundedness" type property (like cardinality) specified in
Theory kinds files; specifies well-foundedness and a ground term
* well-foundedness / finite checks in Datatypes now superseded by type
system isFinite(), isWellFounded(), mkGroundTerm().
* new "RecursionBreaker" template class, a convenient class that keeps
a "seen" trail without you having to pass it around (which is
difficult in cases of mutual recursion) of the idea of passing
around a "seen" trail
|
|
|
