| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
reduce the number of allocations made. Compare cluster jobs 1585 and 1584 for the expected performance increase.
|
|
- Renamed NonZeroIterator to const_iterator.
- Both of these changes are in response to the code review.
|
|
caused a number of latent errors in sources and headers to come up. Those are now fixed (by adding "using" or "std::" depending on the context). Took the opportunity to bring many rewriter sources in line with coding conventions.
|
|
dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine. If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use).
|
|
initialization of the expression variable statistics in last commit
|
|
|
|
created in the expression manager.
this is useful, for example, with --parse-only, to figure out a bit of problem structure
|
