diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-11 15:07:37 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-11 15:07:37 -0600 |
| commit | 7acc2844df65ab6fdbf8166653c71eaa26d4d151 (patch) | |
| tree | e289c79b5cf0bde3f7e261f81fc5c54c58b0ae01 /test/regress/regress0/quantifiers/rew-to-scala.smt2 | |
| parent | 78608a5925938d7ae78b5ac08d2f003d7332810a (diff) | |
More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc.
Diffstat (limited to 'test/regress/regress0/quantifiers/rew-to-scala.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/rew-to-scala.smt2 | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/rew-to-scala.smt2 b/test/regress/regress0/quantifiers/rew-to-scala.smt2 new file mode 100644 index 000000000..1e29241eb --- /dev/null +++ b/test/regress/regress0/quantifiers/rew-to-scala.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((Formula!953 (And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32)))) +)) +(declare-fun error_value!964 () Bool) +(declare-fun isNNF!208 (Formula!953) Bool) +(declare-fun error_value!965 () Formula!953) +(declare-fun nnf!206 (Formula!953) Formula!953) +(declare-fun error_value!966 () Formula!953) +(assert (forall ((f!207 Formula!953)) (= (isNNF!208 f!207) (ite (is-And!954 f!207) (and (and (isNNF!208 (lhs!955 f!207)) (isNNF!208 (lhs!955 f!207))) (isNNF!208 (rhs!956 f!207))) (ite (is-Or!959 f!207) (and (and (isNNF!208 (lhs!960 f!207)) (isNNF!208 (lhs!960 f!207))) (isNNF!208 (rhs!961 f!207))) (ite (is-Not!957 f!207) false (ite (is-Variable!962 f!207) true error_value!964))))) )) +(assert (forall ((formula!205 Formula!953)) (= (nnf!206 formula!205) (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!965)))))))) )) +(assert (exists ((formula!205 Formula!953)) (not (=> (is-Variable!962 formula!205) (isNNF!208 (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!966)))))))))) )) +(check-sat) |