some examples

proofs/eo/cpc/examples/now.eo

@@ -0,0 +1,6 @@
+unsat
+(define @t1 () (str.in_re "a" (str.to_re "b")))
+(assume @p1 @t1)
+(step @p2 :rule str-in-re-consume :args ((= @t1 false)))
+(step @p3 false :rule eq_resolve :premises (@p1 @p2))
+

proofs/eo/cpc/examples/now.ep

@@ -0,0 +1,12 @@
+(include "../rules/Booleans.eo")
+(include "../theories/Ints.eo")
+(include "../programs/Arith.eo")
+(include "../theories/Strings.eo")
+(include "../rules/Strings.eo")
+(include "../programs/Strings.eo")
+(include "../rules/Strings.eo")
+(define @t1 () (str.in_re "a" (str.to_re "b")))
+(assume @p1 @t1)
+(step @p2 :rule str-in-re-consume :args ((= @t1 false)))
+(step @p3 false :rule eq_resolve :premises (@p1 @p2))
+

proofs/eo/cpc/examples/reg_eval.eo

@@ -0,0 +1,5 @@
+(define @t1 () (str.in_re "a" (str.to_re "b")))
+(assume @p1 @t1)
+(step @p2 :rule str-in-re-consume :args ((= @t1 false)))
+(step @p3 false :rule eq_resolve :premises (@p1 @p2))
+

proofs/eo/cpc/examples/reg_eval.smt2

@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (str.in_re "a" (str.to_re "b")))
+(check-sat)

proofs/eo/cpc/examples/run.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+
+# first input -- cvc5 binary
+# second input -- ethos binary
+
+# prepend includes
+echo (include "theories/Ints.eo") > reg_eval.eo
+echo (include "programs/Arith.eo") > reg_eval.eo
+echo (include "theories/Strings.eo") > reg_eval.eo 
+echo (include "rules/Strings.eo") > reg_eval.eo
+echo (include "programs/Strings.eo") > reg_eval.eo
+echo (include "rules/Strings.eo") > reg_eval.eo
+
+# produce proof (remove `unsat` line)
+$1 --dump-proofs --proof-format-mode=cpc --proof-granularity=dsl-rewrite reg_eval.smt2 | tail -n +2 > reg_eval.eo 
+
+
+
+# check the proof
+$2 reg_eval.eo
+
+# check another proof
+ethos tmp.eo

proofs/eo/cpc/examples/tmp.eo

@@ -0,0 +1,9 @@
+(include "theories/Ints.eo")
+(include "programs/Arith.eo")
+(include "theories/Strings.eo")
+(include "rules/Strings.eo")
+(include "programs/Strings.eo")
+(include "rules/Strings.eo")
+
+(step @p1 (= (str.in_re "s" (str.to_re "s")) true) :rule str-in-re-eval :args ((= (str.in_re "s" (str.to_re "s")) true)))
+