threadlocal

Merge from decision branch (till r3663)

(no performace or search behavior changes expected)

small fuzz examples where bv fails

fixing the wrong results. arrays equality adaptor had a missing case when propagating disequalities between shared terms.

LogicInfo locking implemented, and some initialization-order issues in 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.

Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks

Adding EchoCommand and associated printer and parser rules:

* SMT-LIBv2 parser now supports (echo...).
* Dump() gestures can now dump EchoCommands in CVC and SMT-LIB formats.
  This can make it much easier to interpret output.

cleaning up the expample for the future

Added small test case for diseq propagation

fixing some bugs in propagation of disequalities
still doesnt fix the wrong answers thought :(

Don't ever call nonclausalSimplify if simplificationMode = NONE (even if
repeatSimp is true)

Fixed assertion failures

removing std::cout from trunk

also remove now-incorrect comment from makefile

Fixed broken test case, removed one that is a mistake

unconstrained regressions are now run with "make check", but with --unconstrained-simp option

Fixing numerous issues with tests and "make dist":

* test/regress/regress0/unconstrained wasn't being distributed.  This caused the debian build failure last night.  (It still doesn't run on "make check", but had to be distributed properly.)
* Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format.  (Told automake to use a newer tar format.)

disabling a super-expensive assertions to speed up debug runs

Changes to the combination mechanism, lots of details. Not done yet, there 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

Fixed problem causing crash at destruction time

More clean-up

Fixed a performance issue with unconstrained simplifier

Adding missing files...

Added preprocessing pass that propagates unconstrained values - solves all of
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed

add a global user-context push/pop in smt engine, just like clark's addition the other day of a push/pop of the sat context

Fixed bug in bv: one more case where non-shared equality was getting propagated
Added a global push and pop around solving - fixes an assertion failure when
TNodes are still around in a CDHashMap at destruction time.

svn:ignore a parallel-tests driver file that automake deposits in config/

pass JAVA_CPPFLAGS properly

Added BitwiseEq bitvector rewrite
Added option "--repeat-simp" which repeats nonclausal simplification: 4 times,
twice before ite removal and twice after
Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant
speedup on dwp examples

Fixed problem with array queue growing too large

remove unused/broken check build target

removing now-unused TheoryEngine::setLogic() interface function

Enabled SolveEq bv rewrite

Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV

some reordering to keep invariants

Committing the work on equality engine, I need to see how it does on the regressions. New additions:
* areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later.
* propagation of shared dis-equalities (not yet complete, once case missing)
* changes to the theories that use it, authors should check up on the changes

Another expensive function call in a Debug trace

Another expensive function call in a Debug line

init bug fix

Checking in fix for bug 340 - somehow didn't get checked in earlier

Separating the subtheory implementations in the bitvector theory.

Significant changes to the internals of the equality engine. Equality is not handled natively and not as a generic predicate. The changes also change the order of propagation, and can produce different conflicts. Since the engine is now used everywhere this means that so some crazy results are to be expected.

This commit merges in the branch arithmetic/cprop.

Updating equality manager to handle tagged trigger terms. Notifications are pushed out for relationships between terms tagged with the same tag. No performance impact.

main() no longer catches non-CVC4 exceptions.  This means on memout and other C++-level exceptions, we'll exit the C++ way rather than our custom way (so we don't get statistics etc.)

Adding regress test for bug 341.

- The array type rules were fixed to use isSubtypeOf.
- The type of (kind::DIVISION x y) is RealType.
- A reference to util/pseudoboolean.i was removed.
- rec5.cvc is disabled for now.  The type of 2 is Integer which is not a subtype of [0..11].

This commit adds TypeNode::leastCommonTypeNode().  The special case for arithmetic in TypeNode::operator==() has been removed.  A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339

This commit removes the dead psuedoboolean code.

Removing long unsigned operator+ from CDList's const_iterator.

removing failing regression

This fixes a fascinating segfault.  This is the sequence of events:
1) A restart occurs
2) A shared term is registered to arithmetic.
3) Arithmetic sets this up.
4) No new linear relations are added to arithmetic.
5) Eventually a restart occurs.
6) Arithmetic resets the tableau as it has not had a row added since the last restart.
7) A new variable is added.
8) This exceeds the size of the column vector of the saved tableau by exactly one.
9) segfault

Fixing an issue with LogicInfo::isPure() that turned off simplification in QF_UF and maybe others

Fixed bug 338:
   - fixed buggy rewrite rules assuming certain nodes only had 2 children
   - added support for bv-rewrite dump
   - fixed smt2_printer for bv constants

Adding failing regression for ite type computation.

Queueing up asserted literals in the proxy instead of sending them off to the theory engine immediately. The queue is discharged just before a check().

adding simple-minded handling of (dis-)equalities where constants are involved

Fixing C compatibility library (it still had a reference to CONST_INTEGER).

This hopefully fixes the Debian build.

testcase for bug 337

Changes to SAT solver:
* allowing propagation of false literals (handles conflict)
* allowing lemmas during BCP (bug 337)
* UF does direct propagation, without checking for literal value anymore

equality status for bitvectors can now look into the sat solver to check for IN_MODEL status

removing duplicate literals in explanations of propagations

refactored TheoryBV bitblaster and equality engine into subtheories (similar to TheoryEngine

fixed QF_BV performance problem due to using CDList instead of CDQueue

test cases

Fix to shared terms visitor.

Implement TypeNode::isComparableTo() and add a unit test for it.

Fixed several bugs in shared terms database

This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.

renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively

removing all extended commands (as inspired by the Z3 extended command set) except for declare-datatypes

Fix QF_AUFLIA (resolves bug #331).

fixing warnings, grr

several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now term notify handles boolean constants; fixed bug 328

fixes for shared term registration. previously the type was not considered when looking at theories of the term and for a term like

read(a, f(x))

the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail.

Fixed assertion failures in array theory
This fixes bugs 335 and 333.

in debug builds, -d can be used for trace tags that aren't also debug tags

fixing up preregistration again

fixing build warnings

fix regex in Debug_tags and Trace_tags generation for Mac OS

fix typo in sed line

output a warning message when a function type (or datatype, or array, etc.) is created with a Boolean term inside it

Disabled arith-rewrite-equalities by default unless in a pure arithmetic theory

Added some ITE rewrites,
Added ITE simplifier - on by default only for QF_LIA benchmarks
Fixed one bug in arrays
Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()

Partially fixes something-like-a-problem with TheoryArith::getDeltaValue().

Removing now unneeded (as of r3425) typenames from EqualityEngine. trunk now compiles on Debian.

fix an issue which breaks language bindings (so this commit fixes debian nightly builds)

--disable-tracing at configure time now disables Trace() and Debug() gestures both.

* simplifying equality engine interface
* 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

rm something for a future merge that sneaked in

(gets rid of warning)

Merge from decision branch (ITE support)

Major changes from last merge
* ITEs supported
* Don't share theory lemmas to DE, only assertions

Should probably be noted that 'make regress' doesn't quite
pass with --decision=justification. Throws off search in couple
of arith benchmarks.

No serious performance changes expected. Keep an eye.

Fixing the debug tags generation and related methods in configuration.cpp that disallowed me to debug my bugs by reporting that the debug tag doesn't exists, where in fact it was in the code.

1) The grep and sed for tags wasn't picking up on .isOn("tag")
2) The isDebugTag a) didn't take a parameter b) was using binary search using strcmp which is non-portable and didn't work for tags including special characters

Morgan should vet this, since there is some crazy sed stuff going on

Merging in bvprop branch, with proper bit-vector propagation.
This should also fix bug 325.

Fixing a bug with TheoryArith::ppAssert() and shared terms.

Fixes a sign bug in the DioSolver.

Guard for expensive Debug trace

options: fail if the debug or trace tag specified doesn't exist (-d -t)

fix: getNumTraceTags, getNumDebugTags

- This fixes a problem where simplex produced the same conflict in the single check call.
- This increases the number of substitutions that ppAssert can solve on integer equations.