Merge pull request #8 from hansjoergschurr/devel/fix-step-no-proven

Fix nary stuff

proofs/examples/programs.smt2

@@ -1,43 +1,61 @@
 ; Tests for the gerneral programs.
 
 (include "../theories/Core.smt2")
-
-; Proof rule to test if the parameter `test` evaluates to `reference`
-(declare-rule is_equals ((T Type) (test T) (reference T))
- :args (test reference)
- :requires ((test reference))
- :conclusion true
-)
-
 (include "../programs/Nary.smt2")
 
 (declare-const c1 Bool)
 (declare-const c2 Bool)
 (declare-const c3 Bool)
 
 ; Test removeRight
-(step rr1 :rule is_equals :args ((removeRight c1 (or c2 c1)) c2))
-(step rr2 :rule is_equals :args ((removeRight c1 (or c1 c2)) c2))
-(step rr3 :rule is_equals :args ((removeRight c1 (or c1 (or c2 c3))) (or c2 c3)))
-(step rr4 :rule is_equals :args ((removeRight c1 (or c2 (or c1 c3))) (or c2 c3)))
-(step rr5 :rule is_equals :args ((removeRight c1 (or c2 (or c3 c2))) (or c2 c3)))
+(declare-rule check_removeRight((x Bool) (in Bool) (out Bool))
+ :args (x in out)
+ :requires (((removeRight x in) out))
+ :conclusion true
+)
+(step rr1 :rule check_removeRight :args (c1 (or c2 c1) c2))
+(step rr2 :rule check_removeRight :args (c1 (or c1 c2) c2))
+(step rr3 :rule check_removeRight :args (c1 (or c1 (or c2 c3)) (or c2 c3)))
+(step rr4 :rule check_removeRight :args (c1 (or c2 (or c1 c3)) (or c2 c3)))
+(step rr5 :rule check_removeRight :args (c1 (or c2 (or c3 c2)) (or c2 (or c3 c2))))
 
 ; Test appendRight
-(step ar1 :rule is_equals :args ((appendRight or c1 c2) (or c1 c2)))
-(step ar2 :rule is_equals :args ((appendRight or c3 (or c1 c2)) (or c1 (or c2 c3))))
-(step ar3 :rule is_equals :args ((appendRight or c3 (or (or c1 c1) c2)) (or (or c1 c1) (or c2 c3))))
-(step ar4 :rule is_equals :args ((appendRight or c3 (or c1 (or c1 c2))) (or c1 (or c1 (or c2 c3)))))
+(declare-rule check_appendRight((t1 Bool) (t2 Bool) (out Bool))
+ :args (t1 t2 out)
+ :requires (((appendRight or t1 t2) out))
+ :conclusion true
+)
+(step ar1 :rule check_appendRight :args (c1 c2 (or c1 c2)))
+(step ar2 :rule check_appendRight :args (c3 (or c1 c2) (or c3 (or c1 c2))))
+(step ar3 :rule check_appendRight :args (c3 (or (or c1 c1) c2) (or c3 (or (or c1 c1) c2))))
+(step ar4 :rule check_appendRight :args (c3 (or c1 (or c1 c2)) (or c3 (or c1 (or c1 c2)))))
+(step ar5 :rule check_appendRight :args ((or c1 c2) c3 (or c1 (or c2 c3))))
+(step ar6 :rule check_appendRight :args ((or (or c1 c1) c2) c3 (or (or c1 c1) (or c2 c3))))
+(step ar7 :rule check_appendRight :args ((or c1 (or c1 c2)) c3 (or c1 (or c1 (or c2 c3)))))
 
 ; Test removeLeft
-(step rl1 :rule is_equals :args ((removeLeft c1 (or c2 c1)) c2))
-(step rl2 :rule is_equals :args ((removeLeft c1 (or c1 c2)) c2))
-(step rl3 :rule is_equals :args ((removeLeft c1 (or (or c1 c2) c3)) (or c2 c3)))
-(step rl4 :rule is_equals :args ((removeLeft c1 (or (or c2 c1) c3)) (or c2 c3)))
-(step rl5 :rule is_equals :args ((removeLeft c1 (or (or c2 c3) c2)) (or c2 c3)))
+(declare-rule check_removeLeft((x Bool) (in Bool) (out Bool))
+ :args (x in out)
+ :requires (((removeLeft x in) out))
+ :conclusion true
+)
+(step rl1 :rule check_removeLeft :args (c1 (or c2 c1) c2))
+(step rl2 :rule check_removeLeft :args (c1 (or c1 c2) c2))
+(step rl3 :rule check_removeLeft :args (c1 (or (or c1 c2) c3) (or c2 c3)))
+(step rl4 :rule check_removeLeft :args (c1 (or (or c2 c1) c3) (or c2 c3)))
+(step rl5 :rule check_removeLeft :args (c1 (or (or c2 c3) c2) (or (or c2 c3) c2)))
 
 ; Test appendLeft
-(step al1 :rule is_equals :args ((appendLeft or c1 c2) (or c1 c2)))
-(step al2 :rule is_equals :args ((appendLeft or c3 (or c1 c2) ) (or (or c3 c1) c2)))
-(step al3 :rule is_equals :args ((appendLeft or c3 (or (or c1 c1) c2)) (or (or (or c3 c1) c1) c2)))
-(step al4 :rule is_equals :args ((appendLeft or c3 (or c1 (or c1 c2))) (or (or c3 (or c1 c1)) c2)))
+(declare-rule check_appendLeft((t1 Bool) (t2 Bool) (out Bool))
+ :args (t1 t2 out)
+ :requires (((appendLeft or t1 t2) out))
+ :conclusion true
+)
+(step al1 :rule check_appendLeft :args (c1 c2 (or c1 c2)))
+(step al2 :rule check_appendLeft :args (c3 (or c1 c2) (or (or c3 c1) c2)))
+(step al3 :rule check_appendLeft :args (c3 (or (or c1 c1) c2) (or (or (or c3 c1) c1) c2)))
+(step al4 :rule check_appendLeft :args (c3 (or c1 (or c1 c2)) (or (or c3 c1) (or c1 c2))))
+(step al5 :rule check_appendLeft :args ((or c1 c2) c3 (or (or c1 c2) c3)))
+(step al6 :rule check_appendLeft :args ((or (or c1 c1) c2) c3 (or (or (or c1 c1) c2) c3)))
+(step al7 :rule check_appendLeft :args ((or c1 (or c1 c2)) c3 (or (or c1 (or c1 c2)) c3)))
 

proofs/examples/resolution.smt2

@@ -9,7 +9,7 @@
 (assume a3 (not c2))
 
 (step t1 (or c1 c3) :rule resolution :premises (a1 a2) :args (true c2))
-;(step t2 (or c3 c1) :rule resolution :premises (a2 a1) :args (false c2))
+(step t2 (or c3 c1) :rule resolution :premises (a2 a1) :args (false c2))
 
-;(step t3 c1 :rule resolution :premises (a1 a3) :args (true c2))
+(step t3 c1 :rule resolution :premises (a1 a3) :args (true c2))
 

proofs/programs/Nary.smt2

@@ -8,6 +8,7 @@
  ((removeRight t (f u t)) u)
  ((removeRight t (f t u)) u)
  ((removeRight t (f c u)) (f c (removeRight t u)))
+ ((removeRight t c) c)
  )
 )
 
@@ -23,23 +24,25 @@
 )
 
 ; removeLeft t u
-; Remove the first occurence of t from a term u = (f (f (f c1 .. ))
+; Remove the first occurence of t from a term u = f (f (f ... c1) c2 .. )
 (program removeLeft ((T Type) (f (-> T T T)) (t T) (u T) (c T))
  (T T) T
  (
  ((removeLeft t (f t u)) u)
  ((removeLeft t (f u t)) u)
  ((removeLeft t (f u c)) (f (removeLeft t u) c))
+ ((removeLeft t c) c)
  )
 )
 
 ; appendLeft t1 t2
-; Appends a term t2 = (f (f c1 ..)) to a term t1 where f is a
+; Appends a term t2 = (f (f .. c1) c2 ..) to a term t1 where f is a
 ; left-assocative function symbol.
 (program appendLeft ((T Type) (f (-> T T T)) (t1 T) (ts1 T) (t2 T) (ts2 T))
  ((-> T T T) T T) T
  (
- ((appendLeft f (f t1 ts1) t2) (f t2 (appendLeft f t1 ts1)))
- ((appendLeft f t1 ts2 ) (f t1 ts2 ))
+ ((appendLeft f t1 (f ts2 t2)) (f (appendLeft f t1 ts2) t2))
+ ((appendLeft f t1  ts2) (f t1  ts2))
  )
 )
+

src/cmd_parser.cpp

@@ -16,6 +16,7 @@
 #include "cmd_parser.h"
 
 #include <iostream>
+#include <ostream>
 
 namespace alfc {
 
@@ -468,7 +469,9 @@ bool CmdParser::parseNextCommand()
  expected = d_eparser.typeCheck(def);
  if (expected->getKind()!=Kind::PROOF_TYPE)
  {
- d_lex.parseError("Failed to parse proof term");
+ std::stringstream buffer;
+ buffer << "Could not discharge requirements. Got " << expected;
+ d_lex.parseError(buffer.str(), true);
  }
  }
  // bind to variable, note that the definition term is not kept

src/type_checker.cpp

@@ -178,7 +178,7 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream& out)
  }
  if (ctype->getKind()!=Kind::BOOL_TYPE)
  {
-  out << "Non-Bool for argument of Proof";
+ out << "Non-Bool for argument of Proof";
  return nullptr;
  }
  }
@@ -320,7 +320,7 @@ Expr TypeChecker::evaluate(Expr& e)
  Ctx ctx;
  return evaluate(e, ctx);
 }
- 
+
 Expr TypeChecker::evaluate(Expr& e, Ctx& ctx)
 {
  std::unordered_map<Expr, Expr>::iterator it;