Merge branch 'master' into lfscTestslfscTests

10 files changed, 699 insertions, 36 deletions

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index f9631c94d..32901e7ed 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 9c4798898..f0a0b3c3f 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Aina Niemetz, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
new file mode 100644
index 000000000..6e7cabccd
--- /dev/null
+++ b/src/theory/booleans/proof_checker.cpp
@@ -0,0 +1,568 @@
+/*********************                                                        */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of equality proof checker
+ **/
+
+#include "theory/booleans/proof_checker.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+void BoolProofRuleChecker::registerTo(ProofChecker* pc)
+{
+  pc->registerChecker(PfRule::SPLIT, this);
+  pc->registerChecker(PfRule::AND_ELIM, this);
+  pc->registerChecker(PfRule::AND_INTRO, this);
+  pc->registerChecker(PfRule::NOT_OR_ELIM, this);
+  pc->registerChecker(PfRule::IMPLIES_ELIM, this);
+  pc->registerChecker(PfRule::NOT_IMPLIES_ELIM1, this);
+  pc->registerChecker(PfRule::NOT_IMPLIES_ELIM2, this);
+  pc->registerChecker(PfRule::EQUIV_ELIM1, this);
+  pc->registerChecker(PfRule::EQUIV_ELIM2, this);
+  pc->registerChecker(PfRule::NOT_EQUIV_ELIM1, this);
+  pc->registerChecker(PfRule::NOT_EQUIV_ELIM2, this);
+  pc->registerChecker(PfRule::XOR_ELIM1, this);
+  pc->registerChecker(PfRule::XOR_ELIM2, this);
+  pc->registerChecker(PfRule::NOT_XOR_ELIM1, this);
+  pc->registerChecker(PfRule::NOT_XOR_ELIM2, this);
+  pc->registerChecker(PfRule::ITE_ELIM1, this);
+  pc->registerChecker(PfRule::ITE_ELIM2, this);
+  pc->registerChecker(PfRule::NOT_ITE_ELIM1, this);
+  pc->registerChecker(PfRule::NOT_ITE_ELIM2, this);
+  pc->registerChecker(PfRule::NOT_AND, this);
+  pc->registerChecker(PfRule::CNF_AND_POS, this);
+  pc->registerChecker(PfRule::CNF_AND_NEG, this);
+  pc->registerChecker(PfRule::CNF_OR_POS, this);
+  pc->registerChecker(PfRule::CNF_OR_NEG, this);
+  pc->registerChecker(PfRule::CNF_IMPLIES_POS, this);
+  pc->registerChecker(PfRule::CNF_IMPLIES_NEG1, this);
+  pc->registerChecker(PfRule::CNF_IMPLIES_NEG2, this);
+  pc->registerChecker(PfRule::CNF_EQUIV_POS1, this);
+  pc->registerChecker(PfRule::CNF_EQUIV_POS2, this);
+  pc->registerChecker(PfRule::CNF_EQUIV_NEG1, this);
+  pc->registerChecker(PfRule::CNF_EQUIV_NEG2, this);
+  pc->registerChecker(PfRule::CNF_XOR_POS1, this);
+  pc->registerChecker(PfRule::CNF_XOR_POS2, this);
+  pc->registerChecker(PfRule::CNF_XOR_NEG1, this);
+  pc->registerChecker(PfRule::CNF_XOR_NEG2, this);
+  pc->registerChecker(PfRule::CNF_ITE_POS1, this);
+  pc->registerChecker(PfRule::CNF_ITE_POS2, this);
+  pc->registerChecker(PfRule::CNF_ITE_POS3, this);
+  pc->registerChecker(PfRule::CNF_ITE_NEG1, this);
+  pc->registerChecker(PfRule::CNF_ITE_NEG2, this);
+  pc->registerChecker(PfRule::CNF_ITE_NEG3, this);
+}
+
+Node BoolProofRuleChecker::checkInternal(PfRule id,
+                                         const std::vector<Node>& children,
+                                         const std::vector<Node>& args)
+{
+  if (id == PfRule::SPLIT)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, args[0], args[0].notNode());
+  }
+  // natural deduction rules
+  if (id == PfRule::AND_ELIM)
+  {
+    Assert(children.size() == 1);
+    Assert(args.size() == 1);
+    uint32_t i;
+    if (children[0].getKind() != kind::AND || !getUInt32(args[0], i))
+    {
+      return Node::null();
+    }
+    if (i >= children[0].getNumChildren())
+    {
+      return Node::null();
+    }
+    return children[0][i];
+  }
+  if (id == PfRule::AND_INTRO)
+  {
+    Assert(children.size() >= 1);
+    return children.size() == 1
+               ? children[0]
+               : NodeManager::currentNM()->mkNode(kind::AND, children);
+  }
+  if (id == PfRule::NOT_OR_ELIM)
+  {
+    Assert(children.size() == 1);
+    Assert(args.size() == 1);
+    uint32_t i;
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::OR || !getUInt32(args[0], i))
+    {
+      return Node::null();
+    }
+    if (i >= children[0][0].getNumChildren())
+    {
+      return Node::null();
+    }
+    return children[0][0][i].notNode();
+  }
+  if (id == PfRule::IMPLIES_ELIM)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::IMPLIES)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0].notNode(), children[0][1]);
+  }
+  if (id == PfRule::NOT_IMPLIES_ELIM1)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::IMPLIES)
+    {
+      return Node::null();
+    }
+    return children[0][0][0];
+  }
+  if (id == PfRule::NOT_IMPLIES_ELIM2)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::IMPLIES)
+    {
+      return Node::null();
+    }
+    return children[0][0][1].notNode();
+  }
+  if (id == PfRule::EQUIV_ELIM1)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0].notNode(), children[0][1]);
+  }
+  if (id == PfRule::EQUIV_ELIM2)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0], children[0][1].notNode());
+  }
+  if (id == PfRule::NOT_EQUIV_ELIM1)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0][0], children[0][0][1]);
+  }
+  if (id == PfRule::NOT_EQUIV_ELIM2)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
+  }
+  if (id == PfRule::XOR_ELIM1)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::XOR)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0], children[0][1]);
+  }
+  if (id == PfRule::XOR_ELIM2)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::XOR)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0].notNode(), children[0][1].notNode());
+  }
+  if (id == PfRule::NOT_XOR_ELIM1)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::XOR)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0][0], children[0][0][1].notNode());
+  }
+  if (id == PfRule::NOT_XOR_ELIM2)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::XOR)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0][0].notNode(), children[0][0][1]);
+  }
+  if (id == PfRule::ITE_ELIM1)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0].notNode(), children[0][1]);
+  }
+  if (id == PfRule::ITE_ELIM2)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0], children[0][2]);
+  }
+  if (id == PfRule::NOT_ITE_ELIM1)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
+  }
+  if (id == PfRule::NOT_ITE_ELIM2)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, children[0][0][0], children[0][0][2].notNode());
+  }
+  // De Morgan
+  if (id == PfRule::NOT_AND)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT
+        || children[0][0].getKind() != kind::AND)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts;
+    for (unsigned i = 0, size = children[0][0].getNumChildren(); i < size; ++i)
+    {
+      disjuncts.push_back(children[0][0][i].notNode());
+    }
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  // valid clauses rules for Tseitin CNF transformation
+  if (id == PfRule::CNF_AND_POS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 2);
+    uint32_t i;
+    if (args[0].getKind() != kind::AND || !getUInt32(args[1], i))
+    {
+      return Node::null();
+    }
+    if (i >= args[0].getNumChildren())
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, args[0].notNode(), args[0][i]);
+  }
+  if (id == PfRule::CNF_AND_NEG)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::AND)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0]};
+    for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
+    {
+      disjuncts.push_back(args[0][i].notNode());
+    }
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_OR_POS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::OR)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0].notNode()};
+    for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
+    {
+      disjuncts.push_back(args[0][i]);
+    }
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_OR_NEG)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 2);
+    uint32_t i;
+    if (args[0].getKind() != kind::OR || !getUInt32(args[1], i))
+    {
+      return Node::null();
+    }
+    if (i >= args[0].getNumChildren())
+    {
+      return Node::null();
+    }
+    return NodeManager::currentNM()->mkNode(
+        kind::OR, args[0], args[0][i].notNode());
+  }
+  if (id == PfRule::CNF_IMPLIES_POS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::IMPLIES)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{
+        args[0].notNode(), args[0][0].notNode(), args[0][1]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_IMPLIES_NEG1)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::IMPLIES)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0], args[0][0]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_IMPLIES_NEG2)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::IMPLIES)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0], args[0][1].notNode()};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_EQUIV_POS1)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{
+        args[0].notNode(), args[0][0].notNode(), args[0][1]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_EQUIV_POS2)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{
+        args[0].notNode(), args[0][0], args[0][1].notNode()};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_EQUIV_NEG1)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_EQUIV_NEG2)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{
+        args[0], args[0][0].notNode(), args[0][1].notNode()};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_XOR_POS1)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::XOR)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_XOR_POS2)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::XOR)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{
+        args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_XOR_NEG1)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::XOR)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_XOR_NEG2)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::XOR)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_ITE_POS1)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{
+        args[0].notNode(), args[0][0].notNode(), args[0][1]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_ITE_POS2)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_ITE_POS3)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_ITE_NEG1)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{
+        args[0], args[0][0].notNode(), args[0][1].notNode()};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_ITE_NEG2)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::CNF_ITE_NEG3)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    if (args[0].getKind() != kind::ITE)
+    {
+      return Node::null();
+    }
+    std::vector<Node> disjuncts{
+        args[0], args[0][1].notNode(), args[0][2].notNode()};
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  // no rule
+  return Node::null();
+}
+
+}  // namespace booleans
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h
new file mode 100644
index 000000000..8258130fb
--- /dev/null
+++ b/src/theory/booleans/proof_checker.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file proof_checker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Boolean proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H
+#define CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+/** A checker for boolean reasoning in proofs */
+class BoolProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  BoolProofRuleChecker() {}
+  ~BoolProofRuleChecker() {}
+
+  /** Register all rules owned by this rule checker into pc. */
+  void registerTo(ProofChecker* pc) override;
+
+ protected:
+  /** Return the conclusion of the given proof step, or null if it is invalid */
+  Node checkInternal(PfRule id,
+                     const std::vector<Node>& children,
+                     const std::vector<Node>& args) override;
+};
+
+}  // namespace booleans
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H */
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 29f5bb82d..04a1675a4 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index ae498165f..99c80dd4a 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -2,9 +2,9 @@
 /*! \file theory_bool.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Mathias Preiner
+ **   Andres Noetzli, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index ca22467d4..ca2ac13ea 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Dejan Jovanovic, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -157,6 +157,19 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (!done) {
       return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff);
     }
+    // x v ... v x --> x
+    unsigned ind, size;
+    for (ind = 0, size = n.getNumChildren(); ind < size - 1; ++ind)
+    {
+      if (n[ind] != n[ind+1])
+      {
+        break;
+      }
+    }
+    if (ind == size - 1)
+    {
+      return RewriteResponse(REWRITE_AGAIN, n[0]);
+    }
     break;
   }
   case kind::AND: {
@@ -172,6 +185,19 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
       Debug("bool-flatten") << n << ": " << ret.d_node << std::endl;
       return ret;
     }
+    // x ^ ... ^ x --> x
+    unsigned ind, size;
+    for (ind = 0, size = n.getNumChildren(); ind < size - 1; ++ind)
+    {
+      if (n[ind] != n[ind+1])
+      {
+        break;
+      }
+    }
+    if (ind == size - 1)
+    {
+      return RewriteResponse(REWRITE_AGAIN, n[0]);
+    }
     break;
   }
   case kind::IMPLIES: {
@@ -293,28 +319,39 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (n[0].isConst()) {
       if (n[0] == tt) {
         // ITE true x y
-
-        Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl;
+        Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[0] ==tt "
+                          << n << ": " << n[1] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[1]);
       } else {
         Assert(n[0] == ff);
         // ITE false x y
-        Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl;
+        Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[0] ==ff "
+                          << n << ": " << n[1] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[2]);
       }
     } else if (n[1].isConst()) {
       if (n[1] == tt && n[2] == ff) {
-        Debug("bool-ite") << "n[1] ==tt && n[2] == ff " << n << ": " << n[0] << std::endl;
+        Debug("bool-ite")
+            << "TheoryBoolRewriter::preRewrite_ITE: n[1] ==tt && n[2] == ff "
+            << n << ": " << n[0] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[0]);
       }
       else if (n[1] == ff && n[2] == tt) {
-        Debug("bool-ite") << "n[1] ==ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl;
+        Debug("bool-ite")
+            << "TheoryBoolRewriter::preRewrite_ITE: n[1] ==ff && n[2] == tt "
+            << n << ": " << n[0].notNode() << std::endl;
         return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
       }
-      // else if(n[1] == ff){
-      //   Node resp = (n[0].notNode()).andNode(n[2]);
-      //   return RewriteResponse(REWRITE_AGAIN, resp);
-      // }
+      if (n[1] == tt || n[1] == ff)
+      {
+        // ITE C true y --> C v y
+        // ITE C false y --> ~C ^ y
+        Node resp =
+            n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]);
+        Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const "
+                          << n << ": " << resp << std::endl;
+        return RewriteResponse(REWRITE_AGAIN, resp);
+      }
     }
 
     if (n[0].getKind() == kind::NOT)
@@ -324,18 +361,23 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
           REWRITE_AGAIN, nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]));
     }
 
-    // else if (n[2].isConst()) {
-    //   if(n[2] == ff){
-    //     Node resp = (n[0]).andNode(n[1]);
-    //     return RewriteResponse(REWRITE_AGAIN, resp);
-    //   }
-    // }
+    if (n[2].isConst() && (n[2] == tt || n[2] == ff))
+    {
+      // ITE C x true --> ~C v x
+      // ITE C x false --> C ^ x
+      Node resp =
+          n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]);
+      Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const "
+                        << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    }
 
     int parityTmp;
     if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
       Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]);
-      Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp
-                        << " " << n << ": " << resp << std::endl;
+      Debug("bool-ite")
+          << "TheoryBoolRewriter::preRewrite_ITE:  equalityParity n[1], n[2] "
+          << parityTmp << " " << n << ": " << resp << std::endl;
       return RewriteResponse(REWRITE_AGAIN, resp);
     // Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now
     // } else if (n[0].getKind() == kind::NOT) {
@@ -346,15 +388,17 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
 
       // if n[1] is constant this can loop, this is possible in prewrite
       Node resp = n[0].iteNode( (parityTmp == 1) ? tt : ff, n[2]);
-      Debug("bool-ite") << "equalityParity n[0], n[1] " << parityTmp
-                        << " " << n << ": " << resp << std::endl;
+      Debug("bool-ite")
+          << "TheoryBoolRewriter::preRewrite_ITE: equalityParity n[0], n[1] "
+          << parityTmp << " " << n << ": " << resp << std::endl;
       return RewriteResponse(REWRITE_AGAIN, resp);
     } else if(!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0){
       // (parityTmp == 1) if n[0] == n[2]
       // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2]
       Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt);
-      Debug("bool-ite") << "equalityParity n[0], n[2] " << parityTmp
-                        << " " << n << ": " << resp << std::endl;
+      Debug("bool-ite")
+          << "TheoryBoolRewriter::preRewrite_ITE: equalityParity n[0], n[2] "
+          << parityTmp << " " << n << ": " << resp << std::endl;
       return RewriteResponse(REWRITE_AGAIN, resp);
     } else if(n[1].getKind() == kind::ITE &&
               (parityTmp = equalityParity(n[0], n[1][0])) != 0){
@@ -362,8 +406,9 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
       // (parityTmp > 1)  then n : (ite c (ite (not c) x y) z) or
       // n: (ite (not c) (ite c x y) z)
       Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]);
-      Debug("bool-ite") << "equalityParity n[0], n[1][0] " << parityTmp
-                        << " " << n << ": " << resp << std::endl;
+      Debug("bool-ite")
+          << "TheoryBoolRewriter::preRewrite: equalityParity n[0], n[1][0] "
+          << parityTmp << " " << n << ": " << resp << std::endl;
       return RewriteResponse(REWRITE_AGAIN, resp);
     } else if(n[2].getKind() == kind::ITE &&
               (parityTmp = equalityParity(n[0], n[2][0])) != 0){
@@ -371,8 +416,9 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
       // (parityTmp > 1)  then n : (ite c x (ite (not c) y z)) or
       // n: (ite (not c) x (ite c y z))
       Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]);
-      Debug("bool-ite") << "equalityParity n[0], n[2][0] " << parityTmp
-                        << " " << n << ": " << resp << std::endl;
+      Debug("bool-ite")
+          << "TheoryBoolRewriter::preRewrite: equalityParity n[0], n[2][0] "
+          << parityTmp << " " << n << ": " << resp << std::endl;
       return RewriteResponse(REWRITE_AGAIN, resp);
     }
     break;
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index 8fc65932e..04de76ac3 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -2,9 +2,9 @@
 /*! \file theory_bool_rewriter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters, Tim King
+ **   Andres Noetzli, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 18329b8b9..25701d394 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index b0bae3e47..4966afa7d 100644
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -2,9 +2,9 @@
 /*! \file type_enumerator.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King
+ **   Morgan Deters, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim