From 3d4f17ade18a168613b10edc7633923b85852ec3 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 11 May 2011 05:14:36 +0000 Subject: [PATCH] ITE context is mostly bad. Now disabled by default. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1331 e59a4935-1847-0410-ae03-e826735625c1 --- unit_test/ite.smt2 | 42 ------------------------------------------ 1 file changed, 42 deletions(-) delete mode 100644 unit_test/ite.smt2 diff --git a/unit_test/ite.smt2 b/unit_test/ite.smt2 deleted file mode 100644 index ae7f809..0000000 --- a/unit_test/ite.smt2 +++ /dev/null @@ -1,42 +0,0 @@ - -(set-logic QF_BV) -(set-info :smt-lib-version 2.0) -(set-info :category "check") -(set-info :status sat) - -; These can be simplified by considering the context -; of the ITES they contain. - -(declare-fun a () Bool) -(declare-fun b () Bool) -(declare-fun c () Bool) -(assert (ite (or a b) (not (or a b)) c ) ) - -(declare-fun d () Bool) -(declare-fun e () Bool) -(assert (ite (and e d) e (and e d) ) ) - -(declare-fun f () Bool) -(declare-fun g () Bool) -(declare-fun h () Bool) -(assert (ite (or f g) (and g f) g ) ) - -(declare-fun i () Bool) -(declare-fun j () Bool) -(declare-fun k () Bool) -(assert (ite i (ite j i (not i)) i )) - -; This doesn't simplify nicely down yet:: -; 108:(OR -; 50:m -; 52:(AND -; 48:l -; 50:m)) -(declare-fun l () Bool) -(declare-fun m () Bool) -(assert (ite (not (and l m)) m l ) ) - - -(check-sat) -(exit) - -- 2.47.3