QF_LRA, Quantifiers: enable use decision for (only for) stopping search

Fixing bug 360.  The driver wasn't exiting when there was an error (it just plowed ahead to the next command).  Now the driver exits on the first error, unless it's in interactive mode.

QF_AUFLIA: enable use decision for (only for) stopping search

fixing a problem due to lemmas produced while backtracking

--decision=justification-stoponly : use decision engine only for stopping
search early, not to make decisions

new options.h :)

enabling theoryof=term for quantifiers with sharing
disableing one test case in equantifiers/decision that runs long

fixing wrong assertion

Removed assertion that can fail

fixing makefile error that brakes build

Fix array bug causing incorrect answers

small change to equality assertions so that one doesn't get x = y and y = x

Adding the failing QF_AUFLIA regression mentioned in last commit.
pp-regfile.delta02.smt is the one to look at with
--decision=justificaiton, the delta minimized version of pp-regfile,
which also gives wrong answer. due to various commits/fixes, delta01
gives correct answer currently.

This is an attempt to fix the bug in the justification heuristic. The
other minor change is removing dependency of header file in
theory_engine.h

It fixes all known wrong answers in QF_BV and QF_AUFBV. It doesn't fix a
wrong answer for QF_AUFLIA -- it is currently unclear what is the cause
of this bug, could be sharing.

Performance impact (turns out) is none on QF_BV and QF_AUFBV (except, of
course, those for which the answer was wrong earlier; and also perhaps
one or two off-cases)

The issue was with how the infinite loop in justification stuff was prevented.
To keep it short, I skip what was wrong earlier, and this is what is done
now:
* whenever an atomic formula is seen, a list of pairs of <IteSkolemVariable,
  AssertionCorrespondingToIteSkolem> is created for each skolem occuring in
  the atom.
* we iterate over this list, doing the following: check if skolem is marked
  as visited. if not, mark visited, recurse, when back unmark.

I lied, I will tell you what was being done earlier was -- 1. the check for
not being visited was being done in each recursive call, not just for atoms.
2. The AssertionCorrespondingToIteSkolem was being used to check if something
is visited and not IteSkolemVariable. I don't know if this makes any
difference, but anyhow, I think this is cleaner & clearer, so I keep this.

updated build script for smt-comp submission

changing theoryOf in shared mode with arrays to move equalities to arrays
disabled in bitvectors due to non-stably infinite problems

the option to enable it is --theoryof-mode=term

Fixing if condition for trivial equalities in arithmetic. Also some whitespace issues in smt_engine.cpp.

Bug fix in justification heuristic. Had to do with how
a "visited" node in the recursive findSplitter method was
handled (which would lead to infinite loop). Earlier,
they were ignored assuming the ancestor would split on it
later. The right thing to do is to split on it right away.

(Fixes errors from the fuzzer, not the ones from last night's
regression)

Reverting rewrite rule to working version

Fixes some assertion failures

Fix for incompleteness bug with decision engine: repeated simplification
could introduce additional assertions that were not beign processed by the
decision engine.  Now these assertions are merged in with pre-ITE-removal
assertions, ensuring the decision engine sees them.

Fixing mac compilation issues.

one bug fixed

WIP

fixing the problems with the bvminisat. there was a case when things would get bitblasted, it would restart to add the clauses, and loose propagation information.

add failing regression, move error up

Fixing a case for explanation of non-normal form equalities.

bug fixes in justification heuristic
* remove assert iteSkolemMap gives ite-s (not true with repeatSimp)
* handle a corner case in findSplitter triggered by repeatSimp

Fixing a bug related to explaining propagations with non-normalized witnesses.

enabling fixed bug345 case

fixes for the hasTerm issues in the shared database under the decision heuristic

New substitutions implementation - fixes performance issue seen in nonclausal
simplification for some benchmarks

Fixed arithmetic consistency issue.  The simplex conflict variable had to be reenqueued so that the queue was a superset of the failing assertions.  This adds a super expensive debug routine unenqueuedVariablesAreConsistent() that catches this bug.  This is enabled when -d arith::consistency is turned on. make check passes with this flag enabled.

fix for clark's bug
imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get()

don't run rewriterules regressions by default; fixes needed

fix quantifier non-bug

Removed an assertion, unneeded header file

some changes to make CVC4 work nicely with trace executor for application track; (set-option :print-success true) supported, (exit) causes immediate exit regardless of EOF, etc.

making --simplification=none the default for quantified logics; this a request from andy.  evidence of performance improvement: church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4516&reference_id=4475&p=5

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.