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.

Some cleanup starting off from trying to understand the sharing code. 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

Changing d_sharedTermsExist to logicInfo.isSharingEnabled()

Added map from skolem variables to new ite formulas in ite removal.
d_sharedTermsExist is now set based on logicInfo instead of dynamically when
shared terms are found.

New LogicInfo functionality.

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.

require boost library (but not the threading support---that's only necessary for portfolio)

undo, again

adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration manually; this will make the LogicInfo commit coming up much easier to integrate into trunk, and will anyway be cleaned up when quantifiers2 branch is merged into trunk.

undo previous commit (as it will break a number of things without additional support I haven't yet committed)

adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration manually; this will make the LogicInfo commit coming up much easier to integrate into trunk, and will anyway be cleaned up when quantifiers2 branch is merged into trunk.

fix parser logic-handling oversights: QF_UFBV should now be supported

break dependence on zlib-dev for now

Fixed warning in decision_engine.h, minor tweak to caregraph function in
arrays, fixed bug with equalities between constants in shared terms database

This merges in the branch cvc4/branches/arithmetic/matrix into trunk.
- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!

portfolio driver: respect parseOnly option

fix for de+lemmas

for the first time make regress passes even if JH is enabled

This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:
- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager

Merge from decision branch -- partially working justification heuristic

Overview of changes
* command line option --decision={internal,justification}
* justification heuristic handles all operators except ITEs
  revelant stats: decision::jh::*
* if decisionEngine has solved the problem PropEngine returns
  unknown and smtEngine queries DE to get the answer
  relevant stat: smt::resultSource
* there are known bugs

Full list of commits being merged
r3330 use CD data structures in JH
r3329 add command-line option --decision=MODE
r3328 timer stat, other fixes
r3326 more trace
r3325 enable implies, iff, xor (no further regression losses)
r3324 feed decision engine lemmas, changes to quitting mechanism
r3322 In progress
r3321 more fixes...
r3318 bugfix1 (69 more to go)
r3317 Handle other boolean operators in JH (except ITE)
r3316 mechanism for DE to stopSearch
r3315 merge from trunk + JH translation continuation
r3275 change option to enable JH by default[A

Updates to array theory - much more lazy about introduction of reads
Also disabled eager lemmas - slows down QF_AX but gets new examples in QF_AUFBV

In the constructor of DecisionEngine, there were 2 pointers that were assumed to be initialized to NULL. This is not true on all platforms. This is now done explicitly.  Macs builds should now work again.

add the missing BINARY variable in some test/regress makefiles

cout -> warning. Happening in portfolio
rest of the search go through, but still should be investigated

disabling the problematic pragma in node_manager.h on gcc < 4.6 until we figure out what to do with it

Fix for thos annoying "array index" warnings in production builds

A dummy decision engine. Expected performance impact: none.

Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.

Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin

Merges branches/arithmetic/atom-database r2979 through 3247 into trunk.  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.

Fixed bug in sharing with arrays of different types

Fix SExpr name qualification for swig, and #include integer and rational headers.

svn ignore Makefile.in for aufbv regression directory

Adds an operator<< to SExpr::SexprTypes. This fixes bug 317. In debug builds, an Unhandled(SExpr::SexprTypes) could not compile on debian.

merge from arrays-clark branch

* Smt2 printer for datatypes
* Fix DefineFunctionCommand when a constant is defined

* Fix ITEs and functions in CVC language printer.
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
  internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
  SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)

fix distributed builds (and therefore the Debian nightly build) by ignoring Makefile.am files under src/prop/cryptominisat.

processing assertions in bit-vectors even when in fullcheck (needed for sharing)