src/prop/prop_engine.h

   1 /*********************                                           -*- C++ -*-  */
   2 /** prop_engine.h
   3  ** Original author: mdeters
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): dejan
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** The PropEngine (proposiitonal engine); main interface point
  14  ** between CVC4's SMT infrastructure and the SAT solver.
  15  **/
  16
  17 #ifndef __CVC4__PROP_ENGINE_H
  18 #define __CVC4__PROP_ENGINE_H
  19
  20 #include "cvc4_config.h"
  21 #include "expr/node.h"
  22 #include "util/decision_engine.h"
  23 #include "theory/theory_engine.h"
  24 #include "prop/minisat/simp/SimpSolver.h"
  25 #include "prop/minisat/core/SolverTypes.h"
  26
  27 #include <map>
  28
  29 namespace CVC4 {
  30
  31 // In terms of abstraction, this is below (and provides services to)
  32 // Prover and above (and requires the services of) a specific
  33 // propositional solver, DPLL or otherwise.
  34
  35 class PropEngine {
  36   DecisionEngine &d_de;
  37   TheoryEngine &d_te;
  38   CVC4::prop::minisat::SimpSolver d_sat;
  39   std::map<Node, CVC4::prop::minisat::Var> d_vars;
  40   std::map<CVC4::prop::minisat::Var, Node> d_varsReverse;
  41
  42   void addVars(Node);
  43
  44 public:
  45   /**
  46    * Create a PropEngine with a particular decision and theory engine.
  47    */
  48   CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&);
  49
  50   /**
  51    * Converts to CNF if necessary.
  52    */
  53   void solve(Node);
  54
  55 };/* class PropEngine */
  56
  57 }/* CVC4 namespace */
  58
  59 #endif /* __CVC4__PROP_ENGINE_H */