| Age | Commit message (Collapse) | Author |
|---|
|
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development). Dejan has now given me the go-ahead
for a merge.
=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================
Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor. The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead). This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.
TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.
Specifically:
* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
1. As described above.
2. Theories now have const access to the fact queue through base
class functions facts_begin() and facts_end(); useful for
debugging.
* Added an "Asserted" attribute so that theories can check if something
has been asserted or not (and therefore not propagate it). However, this
has been disabled for now, pending more data on the overhead of it, and
pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived! So far mainly infrastructure for having
system tests, but there is a system test aimed at improving code
coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
conformant to CVC4 policy.
Tests have been performed to demonstrate that these changes have no or
negligible effect on performance. In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).
|
|
CDList<> objects that allocate from ContextMemoryAllocator<>. Iterators were broken in that begin() != end() for empty lists (again---only those that allocated space from ContextMemoryAllocator<>). Added a unit test for this, too. Thanks Andy!
|
|
importantly removes an unintentional line of code that had it pivoting more times than intended before rechecking the queue. Importantly, it does this without losing any examples with rewrite-equality enabled. This adds a parameter NUM_CHECKS which determines how many times the queue chould be checked during difference mode. A value of 10 for NUM_CHECKS has been empirically determined to be good in practice. See jobs 1815, 1824, 1825, 1821, 1814.
|
|
|
|
|
|
|
|
|
|
|
|
in a growing vector
|
|
|
|
|
|
Collection mode, the arithmetic priority queue is maintained as a set. Compare jobs 1781 and 1782 for the expected performance change.
|
|
slowing down the search. (The effect can be seen in the difference between jobs 1765 and 1755). This happened during commit -r1480 when adding the ArithStaticLearner. This has been fixed.
|
|
|
|
|
|
- Adds ArithStaticLearner. Consolidates and cleans up the code for static learning in arithmetic. Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick. The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node.
- This commit contains miscellaneous other arithmetic cleanup.
|
|
|
|
CVC4ostream::operator<< should only be executed when d_os != NULL. This was the cause of the NULL pointer dereference in debug builds.
|
|
ueful for me, maybe someone else finds it useful also
|
|
known that x \in {c_i}, then x is not in the interval (c_{i}, c_{i+1}) (assuming the c_i's are sorted). (Compare jobs 1742 and 1739 for the expected performance change on trunk. Compare jobs 1740 and 1738 for the expected performance change with the rewrite-equality patch.)
|
|
set of nodes that are asserted to the theory of the form (=> p_i (= x c_i)). If (or p_1 p_2 ...) is a tautology, then x \in {c_1, c_2, ...}. (This tautology check currently requires CUDD to be installed.) Right now all this does is assert x \leq max{c_i} and x \geq min{c_i}. (Compare jobs 1728 to 1626 for how this affects the miplib examples.)
|
|
|
|
causing a hang in bug220.smt2
|
|
clauses asserting literal would overwrite the propagated literal
let's see if i break the build again
|
|
against cudd libraries, the propositional_query class (in util/),
which uses cudd if it's available (and otherwise answers UNKNOWN for
all queries), and the arith theory support for it (currently disabled
per Tim's request, so he can clean it up).
Other changes include:
* contrib/debug-keys - script to print all used keys under Debug(), Trace()
* test/regress/run_regression - minor fix (don't export a variable)
* configure.ac - replace a comment removed by dejan's google perf commit
* some minor copyright/documentation updates, and minor changes to source
text to make 'clang --analyze' happy.
|
|
enabled at configure with
--with-google-perftools
to use it on ubuntu, you need to install packages google-perftools and libgoogle-perftools0
to run the profiling of the heap, you can run it for example with
HEAPPROFILE=/tmp/profile ./builds/bin/cvc4 test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt
this will create some files /tmp/profile* that you can then
to get the pdf of the profile you can then run
google-pprof --pdf ./builds/bin/cvc4 /tmp/profile.0001.heap > profile.pdf
or for other options check http://goog-perftools.sourceforge.net/doc/
|
|
hopefully this will somewhat alleviate the problem with all the junk files in /tmp
|
|
by 1 to handle the UNDEFINED_KIND case.
|
|
assertion-failure string construction) and addition of an assert_white unit test check for the issue
|
|
Fixed and added bug regression. Thanks Andrew Reynolds for the bug report!
|
|
CodeTimer statistic, and adding a CodeTimer to TheoryEngine::EngineOutputChannel::newFact() for investigation into (possible) slow or redundant theory registration.
|
|
phases of looking for additional conflicts during and after the heuristic pivoting stage. (For the expected performance gain, comparing jobs 1676 and 1643 gives a rough idea.)
|
|
heuristically reset to its initial state during restarts.
|
|
difference is that set.isMember(x) for an ArithVar x s.t. x > set.allocated() returns false for PermissiveBackArithVarSet and is an assertion failure for ArithVarSet. This cuts down on the memory usage of the ColumnMatrix slightly.
|
|
|
|
PreferenceFunction allows for specifying how to choose between two nonbasic variables for which should become basic during the selectSlack(...) function. This partially addresses a point brought up by Dejan during the Code Review. (Unfortunately, function pointers are involved in the implementation. Because of this, I have had Morgan review this code before check-in.)
|
|
|
|
the language: LET now supported (but not "type-lets" yet), OPTION now supported, and ^ operator (exponentiation) supported for nonnegative integer exponents. The latter simply expands to MULT, and of course fails assertions in arithmetic if a variable is raised to n >= 2. Also other CVC parser clean-up.
|
|
|
|
are sent to the sat solver during theory propagation. The lemmas currently come from additional conflicts that are discovered by findConflictOnTheQueue(...).
|
|
|
|
operator=(...) to Tableau.
|
|
|
|
|
|
(now that they are allowed for the datatypes theory, as in (APPLY_CONSTRUCTOR nil) or (APPLY_CONSTRUCTOR zero)). It does this by treating such terms with zero children as non-candidates for congruence, even though they have the congruence kind APPLY_CONSTRUCTOR.
|
|
scripts. Minor changes only, correcting some documentation and fixing some warnings that were being issued about functions not existing.
|
|
|
|
(I think) that Tim found with TimerStat involving wild, sometimes negative, timer statistic values. (It was due to improper initialization.)
|
|
- Adds 3 choices of heuristic variable orders to use in ArithPriorityQueue.
- Adds the pivot-rule command line option.
|
|
Rational>. This addresses a point Dejan brought up in the code review.
|
