From 2dbe1f150d30f0fb0c8522f891104270ce09db4c Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 22 Aug 2014 16:59:28 -0400
Subject: Unsat core infrastruture and API (SMT-LIB compliance to come).

---
 src/proof/proof_manager.h | 63 ++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 52 insertions(+), 11 deletions(-)

(limited to 'src/proof/proof_manager.h')

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index f428de36d..d60a3f6e3 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -20,9 +20,12 @@
 #define __CVC4__PROOF_MANAGER_H
 
 #include <iostream>
+#include <map>
 #include "proof/proof.h"
 #include "util/proof.h"
-
+#include "expr/node.h"
+#include "theory/logic_info.h"
+#include "theory/substitutions.h"
 
 // forward declarations
 namespace Minisat {
@@ -63,6 +66,7 @@ enum ProofFormat {
 std::string append(const std::string& str, uint64_t num);
 
 typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
+typedef std::map < ClauseId, const prop::SatClause* > OrderedIdToClause;
 typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 
@@ -74,6 +78,18 @@ enum ClauseKind {
   LEARNT
 };/* enum ClauseKind */
 
+enum ProofRule {
+  RULE_GIVEN,       /* input assertion */
+  RULE_DERIVED,     /* a "macro" rule */
+  RULE_RECONSTRUCT, /* prove equivalence using another method */
+  RULE_TRUST,       /* trust without evidence (escape hatch until proofs are fully supported) */
+  RULE_INVALID,     /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */
+  RULE_CONFLICT,    /* re-construct as a conflict */
+
+  RULE_ARRAYS_EXT,  /* arrays, extensional */
+  RULE_ARRAYS_ROW,  /* arrays, read-over-write */
+};/* enum ProofRules */
+
 class ProofManager {
   SatProof*    d_satProof;
   CnfProof*    d_cnfProof;
@@ -81,15 +97,25 @@ class ProofManager {
 
   // information that will need to be shared across proofs
   IdToClause d_inputClauses;
-  IdToClause d_theoryLemmas;
+  OrderedIdToClause d_theoryLemmas;
+  IdToClause d_theoryPropagations;
   ExprSet    d_inputFormulas;
-  VarSet     d_propVars;
+  ExprSet    d_inputCoreFormulas;
+  ExprSet    d_outputCoreFormulas;
+  //VarSet     d_propVars;
+
+  int d_nextId;
 
   Proof* d_fullProof;
   ProofFormat d_format; // used for now only in debug builds
 
+  __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction > d_deps;
+
+  // trace dependences back to unsat core
+  void traceDeps(TNode n);
+
 protected:
-  std::string d_logic;
+  LogicInfo d_logic;
 
 public:
   ProofManager(ProofFormat format = LFSC);
@@ -109,35 +135,50 @@ public:
 
   // iterators over data shared by proofs
   typedef IdToClause::const_iterator clause_iterator;
+  typedef OrderedIdToClause::const_iterator ordered_clause_iterator;
   typedef ExprSet::const_iterator assertions_iterator;
   typedef VarSet::const_iterator var_iterator;
 
   clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
   clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
+  size_t num_input_clauses() const { return d_inputClauses.size(); }
 
-  clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
-  clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+  ordered_clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
+  ordered_clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+  size_t num_lemmas() const { return d_theoryLemmas.size(); }
 
   assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); }
   assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
+  size_t num_assertions() const { return d_inputFormulas.size(); }
 
-  var_iterator begin_vars() const { return d_propVars.begin(); }
-  var_iterator end_vars() const { return d_propVars.end(); }
+  void printProof(std::ostream& os, TNode n);
 
-  void addAssertion(Expr formula);
+  void addAssertion(Expr formula, bool inUnsatCore);
   void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
+  // note that n depends on dep (for cores)
+  void addDependence(TNode n, TNode dep);
+
+  assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
+  assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
+  size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
+
+  int nextId() { return d_nextId++; }
 
   // variable prefixes
   static std::string getInputClauseName(ClauseId id);
+  static std::string getLemmaName(ClauseId id);
   static std::string getLemmaClauseName(ClauseId id);
   static std::string getLearntClauseName(ClauseId id);
 
   static std::string getVarName(prop::SatVariable var);
   static std::string getAtomName(prop::SatVariable var);
+  static std::string getAtomName(TNode atom);
   static std::string getLitName(prop::SatLiteral lit);
+  static std::string getLitName(TNode lit);
+
+  void setLogic(const LogicInfo& logic);
+  const std::string getLogic() const { return d_logic.getLogicString(); }
 
-  void setLogic(const std::string& logic_string);
-  const std::string getLogic() const { return d_logic; }
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
-- 
cgit v1.2.3