diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-08-19 23:49:58 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-08-19 23:49:58 +0000 |
| commit | ad24cbdb3462b2b2dd312aab2f1f33d9bbcac00e (patch) | |
| tree | b783098b4d72422826890c46870436cbeae0788d /test/regress/run_regression | |
| parent | 29c72e0fd6d0161de275060bbd05370394f1f708 (diff) | |
UF theory bug fixes, code cleanup, and extra debugging output.
Enabled new UF theory by default.
Added some UF regressions.
Some work on the whole equality-over-bool-removed-in-favor-of-IFF
thing. (Congruence closure module and other things have to handle
IFF as a special case of equality, etc..)
Added pre-rewriting to TheoryBool which rewrites:
* (IFF true x) => x
* (IFF false x) => (NOT x)
* (IFF x true) => x
* (IFF x false) => (NOT x)
* (IFF x x) => true
* (IFF x (NOT x)) => false
* (IFF (NOT x) x) => false
* (ITE true x y) => x
* (ITE false x y) => y
* (ITE cond x x) => x
Added post-rewriting that does all of the above, plus normalize IFF and ITE:
* (IFF x y) => (IFF y x), if y < x
* (ITE (NOT cond) x y) => (ITE cond y x)
(Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.)
A little more debugging output from CNF stream, context pushes/pops,
ITE removal.
Some more documentation.
Fixed some typos.
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index b26792a78..a6ea0797b 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -132,7 +132,7 @@ cvc4base=`basename "$cvc4"` cvc4full="$cvc4dirfull/$cvc4base" echo running $cvc4full `basename "$benchmark"` from `dirname "$benchmark"` ( cd `dirname "$benchmark"`; - "$cvc4full" --segv-nospin `basename "$benchmark"`; + "$cvc4full" -d extra-checking --segv-nospin `basename "$benchmark"`; echo $? >"$exitstatusfile" ) > "$outfile" 2> "$errfile" |