Support for quantifier proofsquantifier_proofs_

14 files changed, 324 insertions, 20 deletions

diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt
index 6e9c8947d..595c077f7 100644
--- a/proofs/signatures/CMakeLists.txt
+++ b/proofs/signatures/CMakeLists.txt
@@ -16,6 +16,7 @@ set(core_signature_files
     th_bv_rewrites.plf
     th_real.plf
     th_int.plf
+    th_quant.plf
 )
 
 set(CORE_SIGNATURES "")
diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf
index 9fa697978..b5bc63d92 100644
--- a/proofs/signatures/th_quant.plf
+++ b/proofs/signatures/th_quant.plf
@@ -14,9 +14,9 @@
        ((apply si1 si2 ti1 ti2) 
            (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
        (default ff)))
+   ((a_var_bv n v) (ifequal ti t tt (ifmarked v (ifequal ti k tt ff) ff)))
    (default (ifequal ti t tt (ifmarked t (ifequal ti k tt ff) ff)))))
 
-
 (program is_inst_f ((fi formula) (f formula) (k term)) bool
   (match f
     ((and f1 f2) (match fi
@@ -51,9 +51,15 @@
     (default ff)))
 
 (program is_inst ((fi formula) (f formula) (t term) (k term)) bool
-  (do (markvar t)
-     (let f1 (is_inst_f fi f k)
-        (do (markvar t) f1))))
+  (match t
+    ((a_var_bv n v) (do (markvar v)
+       (let f1 (is_inst_f fi f k)
+          (do (markvar v) f1))))
+    (default (do (markvar t)
+       (let f1 (is_inst_f fi f k)
+          (do (markvar t) f1))))
+  )
+)
 
 (declare skolem
   (! s sort
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cff31dbcd..d44712dd0 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -145,6 +145,8 @@ libcvc4_add_sources(
   proof/er/er_proof.h
   proof/lemma_proof.cpp
   proof/lemma_proof.h
+  proof/quantifiers_proof.cpp
+  proof/quantifiers_proof.h
   proof/lfsc_proof_printer.cpp
   proof/lfsc_proof_printer.h
   proof/lrat/lrat_proof.cpp
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 18e46a292..20fee83da 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -203,6 +203,13 @@ void BitVectorProof::printOwnedTerm(Expr term,
     return;
   }
 
+  case kind::BOUND_VARIABLE:
+  {
+    os << "(a_var_bv " << utils::getSize(term) << " "
+       << ProofManager::sanitize(term) << ")";
+    return;
+  }
+
   case kind::SKOLEM: {
 
     // TODO: we need to distinguish between "real" skolems (e.g. from array) and "fake" skolems,
@@ -250,7 +257,10 @@ void BitVectorProof::printConstant(Expr term, std::ostream& os)
   Assert (term.isConst());
   os << "(a_bv " << utils::getSize(term) << " ";
 
-  if (d_useConstantLetification) {
+  // TODO: Add BV constants from instantiations to d_constantLetMap.
+  if (d_useConstantLetification
+      && d_constantLetMap.find(term) != d_constantLetMap.end())
+  {
     os << d_constantLetMap[term] << ")";
   } else {
     std::ostringstream paren;
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 005a23378..a8cbb4742 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -25,6 +25,7 @@
 #include "proof/cnf_proof.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/proof_utils.h"
+#include "proof/quantifiers_proof.h"
 #include "proof/resolution_bitvector_proof.h"
 #include "proof/sat_proof_implementation.h"
 #include "proof/theory_proof.h"
@@ -136,6 +137,14 @@ ArithProof* ProofManager::getArithProof() {
   return (ArithProof*)pf;
 }
 
+QuantifiersProof* ProofManager::getQuantifiersProof()
+{
+  Assert(options::proof());
+  TheoryProof* pf =
+      getTheoryProofEngine()->getTheoryProof(theory::THEORY_QUANTIFIERS);
+  return (QuantifiersProof*)pf;
+}
+
 SkolemizationManager* ProofManager::getSkolemizationManager() {
   Assert (options::proof() || options::unsatCores());
   return &(currentPM()->d_skolemizationManager);
@@ -1049,12 +1058,17 @@ void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
   for (unsigned i = 0; i < letOrder.size(); ++i) {
     Expr currentExpr = letOrder[i].expr;
     unsigned letId = letOrder[i].id;
-    ProofLetMap::iterator it = letMap.find(currentExpr);
-    Assert(it != letMap.end());
-    out << "\n(@ let" << letId << " ";
-    d_theoryProof->printBoundTerm(currentExpr, out, letMap);
-    paren << ")";
-    it->second.increment();
+    // TODO: BOUND_VAR_LIST should probably not be filtered out here but not
+    // even appear in the letMap in the first place.
+    if (currentExpr.getKind() != kind::BOUND_VAR_LIST)
+    {
+      ProofLetMap::iterator it = letMap.find(currentExpr);
+      Assert(it != letMap.end());
+      out << "\n(@ let" << letId << " ";
+      d_theoryProof->printBoundTerm(currentExpr, out, letMap);
+      paren << ")";
+      it->second.increment();
+    }
   }
 
   out << std::endl << std::endl;
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 0d3250b12..2d6967c52 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -69,6 +69,7 @@ class TheoryProof;
 class UFProof;
 class ArithProof;
 class ArrayProof;
+class QuantifiersProof;
 
 namespace proof {
 class ResolutionBitVectorProof;
@@ -194,6 +195,7 @@ public:
   static proof::ResolutionBitVectorProof* getBitVectorProof();
   static ArrayProof* getArrayProof();
   static ArithProof* getArithProof();
+  static QuantifiersProof* getQuantifiersProof();
 
   static SkolemizationManager *getSkolemizationManager();
 
diff --git a/src/proof/quantifiers_proof.cpp b/src/proof/quantifiers_proof.cpp
new file mode 100644
index 000000000..6ce314e23
--- /dev/null
+++ b/src/proof/quantifiers_proof.cpp
@@ -0,0 +1,142 @@
+/*********************                                                        */
+/*! \file quantifiers_proof.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Quantifiers proof
+ **
+ ** Quantifiers proof
+ **/
+
+#include "proof/quantifiers_proof.h"
+
+#include "expr/node_manager.h"
+#include "theory/quantifiers/instantiate.h"
+
+namespace CVC4 {
+
+theory::TheoryId QuantifiersProof::getTheoryId()
+{
+  return theory::THEORY_QUANTIFIERS;
+}
+
+Node QuantifiersProof::flattenQuantifier(Node term) const
+{
+  Assert(term.getKind() == kind::FORALL);
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node body = term[1];
+  for (size_t i = 0, size = term[0].getNumChildren(); i < size; i++)
+  {
+    Node variable = term[0][size - i - 1];
+    body = nm->mkNode(
+        kind::FORALL, nm->mkNode(kind::BOUND_VAR_LIST, variable), body);
+  }
+  return body;
+}
+
+void QuantifiersProof::registerTerm(Expr term)
+{
+  // recursively declare all other terms
+  for (size_t i = 0, size = term.getNumChildren(); i < size; ++i)
+  {
+    // could belong to other theories
+    d_proofEngine->registerTerm(term[i]);
+  }
+}
+
+void LFSCQuantifiersProof::printOwnedTerm(Expr term,
+                                          std::ostream& os,
+                                          const ProofLetMap& map)
+{
+  Assert(theory::Theory::theoryOf(term) == theory::THEORY_QUANTIFIERS);
+  switch (term.getKind())
+  {
+    case kind::FORALL:
+    {
+      Assert(term[0].getKind() == kind::BOUND_VAR_LIST);
+      std::ostringstream parens;
+      for (size_t i = 0; i < term[0].getNumChildren(); i++)
+      {
+        os << "(forall _ ";
+        d_proofEngine->printBoundTerm(term[0][i], os, map);
+        os << " ";
+        parens << ")";
+      }
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << parens.str();
+      return;
+    }
+    default: { Unreachable(); }
+  }
+}
+
+void LFSCQuantifiersProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                                 std::ostream& os,
+                                                 std::ostream& paren,
+                                                 const ProofLetMap& map)
+{
+  std::vector<Node> node_lemmas;
+  for (const Expr& expr : lemma)
+  {
+    if (expr.getKind() == kind::NOT && expr[0].getKind() == kind::FORALL)
+    {
+      node_lemmas.push_back(Node::fromExpr(expr));
+    }
+  }
+
+  std::map<Node, Node> quant;
+  std::map<Node, std::vector<Node> > tvec;
+  d_theoryQuantifiers->getQuantifiersEngine()->getExplanationForInstLemmas(
+      node_lemmas, quant, tvec);
+
+  for (const Node& node : node_lemmas)
+  {
+    Assert(node.getKind() == kind::NOT && node[0].getKind() == kind::FORALL);
+    Node flattenedQuantifier = flattenQuantifier(node[0]);
+
+    std::ostringstream parens;
+    const std::vector<Node>& terms = tvec[node];
+    for (size_t i = 0, size = terms.size(); i < size; i++)
+    {
+      Node term = terms[i];
+      os << "(inst _ _ _ ";
+      d_proofEngine->printBoundTerm(term.toExpr(), os, map);
+      os << " ";
+
+      Node var = flattenedQuantifier[0][0];
+      flattenedQuantifier = flattenedQuantifier[1];
+      std::vector<std::pair<Node, Node> > subst = {{var, term}};
+      flattenedQuantifier =
+          flattenedQuantifier.substitute(subst.begin(), subst.end());
+
+      d_proofEngine->printBoundTerm(flattenedQuantifier.toExpr(), os, map);
+      os << " ";
+
+      if (i == 0)
+      {
+        os << ProofManager::getPreprocessedAssertionName(node[0]) << " ";
+      }
+      else
+      {
+        os << "t" << (i - 1) << " ";
+      }
+
+      os << "(\\ t" << i << " ";
+      parens << "))";
+    }
+
+    // TODO: replace with a real proof that shows why the instantiation makes
+    // the body false.
+    os << "(clausify_false (trust_f false))";
+    os << parens.str();
+  }
+}
+
+}  // namespace CVC4
diff --git a/src/proof/quantifiers_proof.h b/src/proof/quantifiers_proof.h
new file mode 100644
index 000000000..cebe4aa30
--- /dev/null
+++ b/src/proof/quantifiers_proof.h
@@ -0,0 +1,86 @@
+/*********************                                                        */
+/*! \file quantifiers_proof.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Quantifiers proof
+ **
+ ** Quantifiers proof
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__QUANTIFIERS_PROOF_H
+#define __CVC4__PROOF__QUANTIFIERS_PROOF_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "proof/theory_proof.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+
+class QuantifiersProof : public TheoryProof
+{
+ protected:
+  theory::quantifiers::TheoryQuantifiers* d_theoryQuantifiers;
+
+ public:
+  QuantifiersProof(theory::quantifiers::TheoryQuantifiers* theoryQuantifiers,
+                   TheoryProofEngine* proofEngine)
+      : TheoryProof(theoryQuantifiers, proofEngine),
+        d_theoryQuantifiers(theoryQuantifiers)
+  {
+  }
+
+  theory::TheoryId getTheoryId() override;
+
+  Node flattenQuantifier(Node term) const;
+  void registerTerm(Expr term) override;
+};
+
+class LFSCQuantifiersProof : public QuantifiersProof
+{
+ public:
+  LFSCQuantifiersProof(
+      theory::quantifiers::TheoryQuantifiers* theoryQuantifiers,
+      TheoryProofEngine* proofEngine)
+      : QuantifiersProof(theoryQuantifiers, proofEngine)
+  {
+  }
+
+  void printOwnedTerm(Expr term,
+                      std::ostream& os,
+                      const ProofLetMap& map) override;
+  void printOwnedSort(Type type, std::ostream& os) override {}
+  void printTheoryLemmaProof(std::vector<Expr>& lemma,
+                             std::ostream& os,
+                             std::ostream& paren,
+                             const ProofLetMap& map) override;
+  void printSortDeclarations(std::ostream& os, std::ostream& paren) override {}
+  void printTermDeclarations(std::ostream& os, std::ostream& paren) override {}
+
+  void printDeferredDeclarations(std::ostream& os, std::ostream& paren) override
+  {
+  }
+
+  void printAliasingDeclarations(std::ostream& os,
+                                 std::ostream& paren,
+                                 const ProofLetMap& globalLetMap) override
+  {
+  }
+};
+
+}  // namespace CVC4
+
+#endif /* __CVC4__PROOF__QUANTIFIERS_PROOF_H */
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index c66aa59e4..52152247b 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -28,6 +28,7 @@
 #include "proof/proof_manager.h"
 #include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
+#include "proof/quantifiers_proof.h"
 #include "proof/resolution_bitvector_proof.h"
 #include "proof/sat_proof.h"
 #include "proof/simplify_boolean_node.h"
@@ -39,6 +40,7 @@
 #include "theory/arrays/theory_arrays.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/output_channel.h"
+#include "theory/quantifiers/theory_quantifiers.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/valuation.h"
@@ -127,6 +129,13 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
         return;
       }
 
+      if (id == theory::THEORY_QUANTIFIERS)
+      {
+        d_theoryProofTable[id] = new LFSCQuantifiersProof(
+            (theory::quantifiers::TheoryQuantifiers*)th, this);
+        return;
+      }
+
       // TODO other theories
     }
   }
@@ -321,6 +330,12 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) {
     return;
   }
 
+  if (type.isBoolean())
+  {
+    getTheoryProof(theory::THEORY_BOOL)->printOwnedSort(type, os);
+    return;
+  }
+
   Unreachable();
 }
 
@@ -1100,12 +1115,11 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   Debug("pf::tp") << "About to delete the theory solver used for proving the lemma: DONE! " << std::endl;
 }
 
-bool TheoryProofEngine::supportedTheory(theory::TheoryId id) {
-  return (id == theory::THEORY_ARRAYS ||
-          id == theory::THEORY_ARITH ||
-          id == theory::THEORY_BV ||
-          id == theory::THEORY_UF ||
-          id == theory::THEORY_BOOL);
+bool TheoryProofEngine::supportedTheory(theory::TheoryId id)
+{
+  return (id == theory::THEORY_ARRAYS || id == theory::THEORY_ARITH
+          || id == theory::THEORY_BV || id == theory::THEORY_UF
+          || id == theory::THEORY_BOOL || id == theory::THEORY_QUANTIFIERS);
 }
 
 bool TheoryProofEngine::printsAsBool(const Node &n) {
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 10823693d..19d72d99d 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -620,9 +620,10 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
 
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
 
-  if (term.getKind() == kind::VARIABLE ||
-      term.getKind() == kind::SKOLEM ||
-      term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
+  if (term.getKind() == kind::VARIABLE || term.getKind() == kind::SKOLEM
+      || term.getKind() == kind::BOOLEAN_TERM_VARIABLE
+      || term.getKind() == kind::BOUND_VARIABLE)
+  {
     os << term;
     return;
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d035f88c1..bc3211a17 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4432,6 +4432,8 @@ void SmtEngine::checkProof()
           // Pure logics
           logicString == "QF_UF" || logicString == "QF_AX"
           || logicString == "QF_BV" ||
+          // Quantified pure logics
+          logicString == "UF" || logicString == "BV" ||
           // Non-pure logics
           logicString == "QF_AUF" || logicString == "QF_UFBV"
           || logicString == "QF_ABV" || logicString == "QF_AUFBV"))
diff --git a/test/regress/regress0/quantifiers/simple_quant_proof.smt2 b/test/regress/regress0/quantifiers/simple_quant_proof.smt2
new file mode 100644
index 000000000..a63eaf926
--- /dev/null
+++ b/test/regress/regress0/quantifiers/simple_quant_proof.smt2
@@ -0,0 +1,8 @@
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 2))
+(assert
+   (forall
+    ((A (_ BitVec 2)))
+      (= #b11 (bvadd A #b01))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/simple_quant_proof2.smt2 b/test/regress/regress0/quantifiers/simple_quant_proof2.smt2
new file mode 100644
index 000000000..bf0e2b303
--- /dev/null
+++ b/test/regress/regress0/quantifiers/simple_quant_proof2.smt2
@@ -0,0 +1,8 @@
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 2))
+(assert
+   (forall
+    ((A (_ BitVec 2)) (B (_ BitVec 2)))
+      (= A B)))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/simple_quant_proof3.smt2 b/test/regress/regress0/quantifiers/simple_quant_proof3.smt2
new file mode 100644
index 000000000..2e4244e0b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/simple_quant_proof3.smt2
@@ -0,0 +1,8 @@
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 2))
+(assert
+   (forall
+    ((A (_ BitVec 2)) (B (_ BitVec 2)))
+      (and (= A B) (= A (bvadd B #b01)))))
+(check-sat)