List attributes, fix type checker

src/expr_parser.cpp

@@ -437,6 +437,10 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList()
  t = parseType();
  Expr v = d_state.mkVar(name, t);
  bind(name, v);
+ // parse attribute list
+ std::map<Attr, Expr> attrs;
+ parseAttributeList(v, attrs);
+ d_state.markAttributes(v, attrs);
  d_lex.eatToken(Token::RPAREN);
  }
  return varList;
@@ -558,6 +562,7 @@ void ExprParser::parseAttributeList(const Expr& e, std::map<Attr, Expr>& attrs)
  case Attr::RIGHT_ASSOC:
  case Attr::LEFT_ASSOC:
  case Attr::CHAINABLE:
+ case Attr::PAIRWISE:
  {
  // optional value
  Token tok = d_lex.peekToken();

src/state.cpp

@@ -144,6 +144,7 @@ Expr State::mkSymbolInternal(Kind k, const std::string& name, const Expr& type)
  // type is stored as a child
  Expr v = mkExprInternal(k, {}, false);
  // immediately set its type
+ // FIXME: evaluate?
  v->d_type = type;
  // map to the data
  ExprInfo* ei = getOrMkInfo(v.get());
@@ -173,7 +174,7 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
  case Attr::RIGHT_ASSOC:
  {
  size_t nchild = children.size();
- if (nchild>3)
+ if (nchild>2)
  {
  bool isLeft = (ai->d_attrCons==Attr::LEFT_ASSOC);
  Expr hd = children[0];
@@ -185,7 +186,7 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
  if (ai->d_attrConsTerm!=nullptr)
  {
  AppInfo * ail = getAppInfo(curr.get());
- if (ail!=nullptr && !ail->hasAttribute(Attr::LIST))
+ if (ail==nullptr || !ail->hasAttribute(Attr::LIST))
  {
  // if the last term is not marked as a list variable and
  // we have a null terminator, then we insert the null terminator

src/state.h

@@ -82,12 +82,12 @@ class State
  bool hasProgram(const Expr& v) const;
  /** Maybe evaluate */
  Expr evaluate(const std::vector<Expr>& children, Ctx& newCtx);
+ /** */
+ Expr mkExprInternal(Kind k, const std::vector<Expr>& children, bool doHash=true);
 private:
  /** */
  Expr mkSymbolInternal(Kind k, const std::string& name, const Expr& type);
  /** */
- Expr mkExprInternal(Kind k, const std::vector<Expr>& children, bool doHash=true);
- /** */
  AppInfo* getAppInfo(const ExprValue* e);
  /** 
  * Bind builtin

src/type_checker.cpp

@@ -469,7 +469,7 @@ Expr TypeChecker::evaluate(Expr& e, Ctx& ctx)
  }
  if (evaluated==nullptr)
  {
- evaluated = d_state.mkExpr(cur->getKind(), cchildren);
+ evaluated = d_state.mkExprInternal(cur->getKind(), cchildren);
  }
  // remember its type?
  //evaluated->d_type = cur->d_type;

tests/or-list-null-term.smt2

@@ -7,12 +7,12 @@
 (declare-const a Bool)
 (declare-const b Bool)
 
-(declare-rule and_elim1 ((f Bool) (g Bool))
+(declare-rule and_elim1 ((f Bool) (g Bool :list))
  :premises ((and f g))
  :args ()
  :conclusion f
 )
-(declare-rule or_elim1 ((f Bool) (g Bool))
+(declare-rule or_elim1 ((f Bool :list) (g Bool))
  :premises ((or f g))
  :args ()
  :conclusion f

tests/or-repl-all-basic.smt2

@@ -0,0 +1,32 @@
+
+(declare-const false Bool)
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(declare-const or (-> Bool Bool Bool) :right-assoc)
+
+(program replAll 
+ ((x Bool) (y Bool) (z Bool) (tail Bool :list))
+ (Bool Bool Bool) Bool
+ ; cases
+ (
+ ((replAll x y (or x tail)) (or y (replAll x y tail)))
+ ((replAll x y (or z tail)) (or z (replAll x y tail)))
+ ((replAll x y z) z)
+ )
+)
+
+(declare-rule or_repl-all 
+ ((f Bool) (a Bool) (b Bool))
+ :premises (f (= a b))
+ :args ()
+ :conclusion (replAll a b f)
+)
+
+(declare-const a Bool)
+(declare-const b Bool)
+(assume a1 (or a b b a b))
+(assume a2 (= a b))
+(step a3 (or b b b b b) :rule or_repl-all :premises (a1 a2))
+
+
+

tests/or-repl-all.smt2

@@ -0,0 +1,39 @@
+
+(declare-const false Bool)
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(declare-const or (-> Bool Bool Bool) :right-assoc false)
+
+(program append 
+ ((h Bool) (t Bool :list))
+ (Bool Bool) Bool
+ (
+ ((append h t) (or h t))
+ )
+)
+
+(program replAll 
+ ((x Bool) (y Bool) (z Bool) (tail Bool :list))
+ (Bool Bool Bool) Bool
+ (
+ ((replAll x y (or x tail)) (append y (replAll x y tail)))
+ ((replAll x y (or z tail)) (append z (replAll x y tail)))
+ ((replAll x y z) z)
+ )
+)
+
+(declare-rule or_repl-all 
+ ((f Bool) (a Bool) (b Bool))
+ :premises (f (= a b))
+ :args ()
+ :conclusion (replAll a b f)
+)
+
+(declare-const a Bool)
+(declare-const b Bool)
+(assume a1 (or a b b a b))
+(assume a2 (= a b))
+(step a3 (or b b b b b) :rule or_repl-all :premises (a1 a2))
+
+
+