bug ifx, mv

restore destruction of stuff in driver

This commit:
* enables decision heuristic (justification) for QF_BV and QF_AUFBV
* disables a failing regression in aufbv (because of equality engine
  assert failure trigerred by above change)
* moves around the init procedure smt_engine
* destruction time issues because of moving this -- still to be fixed,
  currently get around by not destucting stuff in driver

failing quantifier

The "no-tears-in-competition-mode" commit.  Change all (non-driver, non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.

fix cout, fix statname, rm deadcode

add passing regression

changing to a more natural propagation order in uf, seems to pay off

some changes to the uf engine
* dramatically less terms to manage by doing reflexivity semantically
* fixes the problem clark had with not detecting inconsistencies with shared terms
i'm not sure what's the performance impact, but this is so much better and we'll deal with performance later

Brings the tuning branch into trunk. This includes the changes from restricted-simplex.

bug 346 resolved

* removing rewriteEquality from the rewriter
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized

removing bug233 until morgan commits the actual file

adding some regressions to the usual regressions runs; several recently-fixed incremental bugs are closed

Added witnesses to Constraints.

- Added a loop to internally assert constraints that are marked as true.
- Changes how CongruenceManager reports conflicts.
- ConstraintDatabase can now detect and raise conflicts when doing unate propagation.

Fixed whitespace warning on Makefile.

Adds debugging output to theory_engine.cpp.

revisions to the "make submission" target

Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow condition when reading from stdin.  This should completely resolve bug #319.

However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track).
So I updated the submission script and competition build so that
* a competition build with antlr-inlining is built for the main and parallel tracks
* a competition build without antlr-inlining is built for the application track

Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works).  For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds.

Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree.

Closing bug #319.

add passing regression

fix for bug 354

Fixed failing assertion when EqualityEngine is in conflict

enabling regressions from last night, all fixed

enable some decision regressions

Make d_result in DE context dependent

(fixes bugs in bv, others with JH on)

Fixed definition of bvsmod

decision regressions, all but one fail

Fixes more problems in bv rewrites

!(*child_it).isConst() assertion fail
this is delta minimal with the same assertion

r2.node == response.node failure

r2.node == response.node failure

!current[0].isConst() failure

Fixes lots of problems in bv rewrite rules and adds lots of assertions
to catch any that I may have missed

benchmark to show that we don't rewrite bvsmod correctly
the definition in smtlib was buggy and was changed on 2011-06-15
check http://goedel.cs.uiowa.edu/smtlib/logics/QF_BV.smt2

Fix some compile warnings (but they never showed up on church)

Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but other *UF* logics do not (e.g. QF_UFLIA).

Also fix a syntax error in a regression test (CVC4 is too lenient to catch it though---CVC3 tripped over it).

Also add additional parts for "make submission" in the top-level makefile

missing problems

wrong answer for bv

Moved some things around in the preprocessor.  Now theory preprocessing gets
called before ite simplification unless arithrewriteequality is on

Fixed fuzzing bug

Fix to yesterday's change in arithmetic.

bv reduced with decision: sat instead of unsat

Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justification

bufixes and the bugs

* array now only propagates thropugh the equality engine
* assertions in the equality rewriting to ensure eq -> { eq, T, F }

conflicts from theories are removable

Changed bitvector theory rewriter so that equalities always get rewritten to
equalities or true or false

cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we were seeing in quantifiers+decision stuff

Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and QF_LIA/solver_cvc4/incorrect3.smt

Fixed failing assertion in arrays for bug 347

more breakage in aufbv

Assertion `value(l) == (lbool((uint8_t)0))' failed.

and

d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()

minor cleanup, and replace a "private:" in equality engine that had been removed by the quantifiers merge (I had reengineered some things from quantifiers so that the equality engine didn't have to expose internals as public, but then had neglected to re-privatize them)

Fixed compile error

Enabling constant propagation

fix a few compatibility bindings issues

wrong answer benchmarks
these should be simple constant propagation problems

wrong result benchmark

tests for the

!isEliminated(var(ps[i]))

assert fails

test cases for the

d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()

assertion fail

Adding constant propagation code - needs more testing - off by default

Adding incorrect qf_lia result.

fix ordering issue of --dump-to and --default-dag-thresh.  now can be specified in either order and the DAG threshold takes.

Fix to term normalization of integer equalities. Adds a regression test that triggered it.

Fixing type comparision assertion in getEqualityStatus().

another benchmark that used to fail

fixing bitvector bugs
* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally

mark a quantifiers global var as "static" so we can find it easier later

OK, now the rewrite issues are fixed

distribute an .expect file.  fixes a "make check" failure not for svn working dirs but for distributed tarballs.

Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

Fix for array bug with decision heuristic
Also fixed one bv rewrite failure (more to come)

fix issue referred to in bug 352 regarding infinite loop between SubstitutionMap (when debugging tag "substitutions" is on) and DagificationVisitor

failing bv examples

Fixed bug 352

some failing examples

Fixed one more bug in rewriter

Added a very fruitful assertion to the rewriter: checks that rewriting after "REWRITE_DONE" is idempotent
Found several problems where this is not the case and fixed them

adding an assertion to trigger the problem of bug349 and the testcase
bv rewriter apparently deosn't have a proper normal form for equalities

fixes for bug347
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately

Turning on unconstrained simp for QF_AUFBV

Cleanup and comments for the dag-ifier.  Also some unit testing for it.

Dagification of output expressions.

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.

The option --arith-presolve-lemmas had previously been renamed --unate-lemmas.

This commit just renames it in --help documentation, etc.

Extend Printer infrastructure also to the "Result" class, meaning that different output languages can write "sat", "unsat", etc., in different ways.  No output is changed by this commit, but the flexibility is added that Francois wanted at today's meeting.

minor fixes, for Mac OS

very small fast example for the bv fail

Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier).

handle BitVectorSignExtend in pickler

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