More

6 files changed, 47 insertions, 16 deletions

diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp
index 1a5eeb86e..251ba23f7 100644
--- a/src/theory/uf/proof_checker.cpp
+++ b/src/theory/uf/proof_checker.cpp
@@ -20,7 +20,7 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-Node EqProofRuleChecker::check(PfRule id,
+Node UfProofRuleChecker::check(PfRule id,
                                const std::vector<Node>& children,
                                const std::vector<Node>& args)
 {
@@ -144,6 +144,33 @@ Node EqProofRuleChecker::check(PfRule id,
     }
     return children[0];
   }
+  else if (id==PfRule::MACRO_EQ_SUBS_REWRITE)
+  {
+    Assert(args.size()==2);
+    // (TRANS (SUBS_REWRITE <children> <args>[0]) 
+    //        (SYMM (SUBS_REWRITE <children> <args>[1])))
+    Node conc1 = d_builtinChecker.checkChildrenArg(PfRule::SUBS_REWRITE,children,args[0]);
+    if (conc1.isNull())
+    {
+      return Node::null();
+    }
+    Node conc2 = d_builtinChecker.checkChildrenArg(PfRule::SUBS_REWRITE,children,args[1]);
+    if (conc2.isNull())
+    {
+      return Node::null();
+    }
+    Node symConc2 = checkChild(PfRule::SYMM, conc2);
+    if (symConc2.isNull())
+    {
+      return Node::null();
+    }
+    std::vector<Node> tchildren = {conc1,symConc2};
+    return checkChildren(PfRule::TRANS,tchildren);
+  }
+  else if (id==PfRule::MACRO_REWRITE_PRED)
+  {
+    
+  }
   // no rule
   return Node::null();
 }
diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h
index 853fb85f1..8e5bb67a1 100644
--- a/src/theory/uf/proof_checker.h
+++ b/src/theory/uf/proof_checker.h
@@ -20,21 +20,25 @@
 #include "expr/node.h"
 #include "expr/proof_checker.h"
 #include "expr/proof_node.h"
+#include "theory/builtin/proof_checker.h"
 
 namespace CVC4 {
 namespace theory {
 namespace uf {
 
 /** A checker for builtin proofs */
-class EqProofRuleChecker : public ProofRuleChecker
+class UfProofRuleChecker : public ProofRuleChecker
 {
  public:
-  EqProofRuleChecker() {}
-  ~EqProofRuleChecker() {}
+  UfProofRuleChecker() {}
+  ~UfProofRuleChecker() {}
   /** Return the conclusion of the given proof step, or null if it is invalid */
   Node check(PfRule id,
              const std::vector<Node>& children,
              const std::vector<Node>& args) override;
+ private:
+  /** Builtin proof checker */
+  builtin::BuiltinProofRuleChecker d_builtinChecker;
 };
 
 }  // namespace uf
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index f38d426ff..2a3d3d0c9 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -428,9 +428,9 @@ std::ostream& operator<<(std::ostream& out, const ProofInferInfo& pii)
   {
     out << " :args (" << pii.d_args << ")";
   }
-  if (!pii.d_childrenExp.empty())
+  if (!pii.d_childrenToExplain.empty())
   {
-    out << " :childrenExp (" << pii.d_childrenExp << ")";
+    out << " :childrenExp (" << pii.d_childrenToExplain << ")";
   }
   out << ")";
   return out;
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 640bcae81..696edab98 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -207,7 +207,7 @@ class ProofInferInfo
   /** The proof arguments */
   std::vector<Node> d_args;
   /** The children to explain */
-  std::vector<Node> d_childrenExp;
+  std::vector<Node> d_childrenToExplain;
 };
 
 /**
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2e693a468..430d88835 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -70,14 +70,14 @@ void TheoryUF::setProofChecker(ProofChecker* pc)
 {
   Assert(pc != nullptr);
   // add checkers
-  pc->registerChecker(PfRule::REFL, &d_eqProofChecker);
-  pc->registerChecker(PfRule::SYMM, &d_eqProofChecker);
-  pc->registerChecker(PfRule::TRANS, &d_eqProofChecker);
-  pc->registerChecker(PfRule::CONG, &d_eqProofChecker);
-  pc->registerChecker(PfRule::TRUE_INTRO, &d_eqProofChecker);
-  pc->registerChecker(PfRule::TRUE_ELIM, &d_eqProofChecker);
-  pc->registerChecker(PfRule::FALSE_INTRO, &d_eqProofChecker);
-  pc->registerChecker(PfRule::FALSE_ELIM, &d_eqProofChecker);
+  pc->registerChecker(PfRule::REFL, &d_ufProofChecker);
+  pc->registerChecker(PfRule::SYMM, &d_ufProofChecker);
+  pc->registerChecker(PfRule::TRANS, &d_ufProofChecker);
+  pc->registerChecker(PfRule::CONG, &d_ufProofChecker);
+  pc->registerChecker(PfRule::TRUE_INTRO, &d_ufProofChecker);
+  pc->registerChecker(PfRule::TRUE_ELIM, &d_ufProofChecker);
+  pc->registerChecker(PfRule::FALSE_INTRO, &d_ufProofChecker);
+  pc->registerChecker(PfRule::FALSE_ELIM, &d_ufProofChecker);
 }
 
 void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 6ae28732f..49fa2e4f8 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -232,7 +232,7 @@ private:
 
   TheoryUfRewriter d_rewriter;
   /** Proof rule checker */
-  EqProofRuleChecker d_eqProofChecker;
+  UfProofRuleChecker d_ufProofChecker;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */