big update, better formalization for pegsol

[ar1516.git] / a2 / src / 1.bash

diff --git a/a2/src/1.bash b/a2/src/1.bash
deleted file mode 100755 (executable)
index b1e02ff..0000000
--- a/a2/src/1.bash
+++ /dev/null
@@ -1,50 +0,0 @@
-#!/bin/bash
-AI=40
-BI=30
-CI=145
-TI=300
-AMAX=120
-BMAX=120
-CMAX=200
-TMAX=300
-
-ITERATIONS=1
-
-function generate {
-       cat<<GEN
-(benchmark a1.smt
-:logic QF_UFLIA
-:extrafuns (
-$(     for i in $(seq 0 $ITERATIONS); do
-               echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
-       done)
-)
-:formula
-(and
-       -- PRECONDITION
-       (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TI) (= l0 0) (= d0 0))
-GEN
-       for i in $(seq 1 $ITERATIONS); do
-               cat<<GEN
-       -- SPECIAL CASE FOR STATE S(0)
-       (= l$i 0) (= d$i 0) (= t$i $TMAX)
-       (or
-               (and -- Comes from A
-                       (= l$((i-1)) 1)
-                       (= a$i (- a$((i-1)) 29)
-                       (= b$i (- b$((i-1)) 29)
-                       (= c$i (- c$((i-1)) 29)
-               )
-               (and -- Comes from B
-                       (= l$((i-1)) 2)
-                       (= a$i (- a$((i-1)) 21)
-                       (= b$i (- b$((i-1)) 21)
-                       (= c$i (- c$((i-1)) 21)
-               )
-       )
-GEN
-       done
-       echo "))"
-}
-#time generate | yices-smt -m | python3 src/a2.py > $1
-generate