src/prop/prop_engine.h

   1 /*********************                                                        */
   2 /*! \file prop_engine.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Dejan Jovanovic, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The PropEngine (propositional engine); main interface point
  13  ** between CVC4's SMT infrastructure and the SAT solver
  14  **
  15  ** The PropEngine (propositional engine); main interface point
  16  ** between CVC4's SMT infrastructure and the SAT solver.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef CVC4__PROP_ENGINE_H
  22 #define CVC4__PROP_ENGINE_H
  23
  24 #include <sys/time.h>
  25
  26 #include "base/modal_exception.h"
  27 #include "expr/node.h"
  28 #include "options/options.h"
  29 #include "preprocessing/assertion_pipeline.h"
  30 #include "proof/proof_manager.h"
  31 #include "prop/minisat/core/Solver.h"
  32 #include "prop/minisat/minisat.h"
  33 #include "prop/proof_cnf_stream.h"
  34 #include "prop/prop_proof_manager.h"
  35 #include "prop/sat_solver_types.h"
  36 #include "theory/trust_node.h"
  37 #include "util/resource_manager.h"
  38 #include "util/result.h"
  39 #include "util/unsafe_interrupt_exception.h"
  40
  41 namespace CVC4 {
  42
  43 class ResourceManager;
  44 class DecisionEngine;
  45 class OutputManager;
  46 class TheoryEngine;
  47
  48 namespace theory {
  49   class TheoryRegistrar;
  50 }/* CVC4::theory namespace */
  51
  52 namespace prop {
  53
  54 class CnfStream;
  55 class CDCLTSatSolverInterface;
  56
  57 class PropEngine;
  58
  59 /**
  60  * PropEngine is the abstraction of a Sat Solver, providing methods for
  61  * solving the SAT problem and conversion to CNF (via the CnfStream).
  62  */
  63 class PropEngine
  64 {
  65  public:
  66   /**
  67    * Create a PropEngine with a particular decision and theory engine.
  68    */
  69   PropEngine(TheoryEngine*,
  70              context::Context* satContext,
  71              context::UserContext* userContext,
  72              ResourceManager* rm,
  73              OutputManager& outMgr,
  74              ProofNodeManager* pnm);
  75
  76   /**
  77    * Destructor.
  78    */
  79   CVC4_PUBLIC ~PropEngine();
  80
  81   /**
  82    * Finish initialize. Call this after construction just before we are
  83    * ready to use this class. Should be called after TheoryEngine::finishInit.
  84    * This method converts and asserts true and false into the CNF stream.
  85    */
  86   void finishInit();
  87
  88   /**
  89    * This is called by SmtEngine, at shutdown time, just before
  90    * destruction.  It is important because there are destruction
  91    * ordering issues between some parts of the system (notably between
  92    * PropEngine and Theory).  For now, there's nothing to do here in
  93    * the PropEngine.
  94    */
  95   void shutdown() {}
  96
  97   /**
  98    * Preprocess the given node. Return the REWRITE trust node corresponding to
  99    * rewriting node. New lemmas and skolems are added to ppLemmas and
 100    * ppSkolems respectively.
 101    *
 102    * @param node The assertion to preprocess,
 103    * @param ppLemmas The lemmas to add to the set of assertions,
 104    * @param ppSkolems The skolems that newLemmas correspond to,
 105    * @return The (REWRITE) trust node corresponding to rewritten node via
 106    * preprocessing.
 107    */
 108   theory::TrustNode preprocess(TNode node,
 109                                std::vector<theory::TrustNode>& ppLemmas,
 110                                std::vector<Node>& ppSkolems);
 111   /**
 112    * Remove term ITEs (and more generally, term formulas) from the given node.
 113    * Return the REWRITE trust node corresponding to rewriting node. New lemmas
 114    * and skolems are added to ppLemmas and ppSkolems respectively. This can
 115    * be seen a subset of the above preprocess method, which also does theory
 116    * preprocessing and rewriting.
 117    *
 118    * @param node The assertion to preprocess,
 119    * @param ppLemmas The lemmas to add to the set of assertions,
 120    * @param ppSkolems The skolems that newLemmas correspond to,
 121    * @return The (REWRITE) trust node corresponding to rewritten node via
 122    * preprocessing.
 123    */
 124   theory::TrustNode removeItes(TNode node,
 125                                std::vector<theory::TrustNode>& ppLemmas,
 126                                std::vector<Node>& ppSkolems);
 127   /**
 128    * Notify preprocessed assertions. This method is called just before the
 129    * assertions are asserted to this prop engine. This method notifies the
 130    * decision engine and the theory engine of the assertions in ap.
 131    */
 132   void notifyPreprocessedAssertions(const preprocessing::AssertionPipeline& ap);
 133
 134   /**
 135    * Converts the given formula to CNF and assert the CNF to the SAT solver.
 136    * The formula is asserted permanently for the current context.
 137    * @param node the formula to assert
 138    */
 139   void assertFormula(TNode node);
 140
 141   /**
 142    * Converts the given formula to CNF and assert the CNF to the SAT solver.
 143    * The formula can be removed by the SAT solver after backtracking lower
 144    * than the (SAT and SMT) level at which it was asserted.
 145    *
 146    * @param trn the trust node storing the formula to assert
 147    * @param p the properties of the lemma
 148    */
 149   void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
 150
 151   /**
 152    * If ever n is decided upon, it must be in the given phase.  This
 153    * occurs *globally*, i.e., even if the literal is untranslated by
 154    * user pop and retranslated, it keeps this phase.  The associated
 155    * variable will _always_ be phase-locked.
 156    *
 157    * @param n the node in question; must have an associated SAT literal
 158    * @param phase the phase to use
 159    */
 160   void requirePhase(TNode n, bool phase);
 161
 162   /**
 163    * Return whether the given literal is a SAT decision.  Either phase
 164    * is permitted; that is, if "lit" is a SAT decision, this function
 165    * returns true for both lit and the negation of lit.
 166    */
 167   bool isDecision(Node lit) const;
 168
 169   /**
 170    * Checks the current context for satisfiability.
 171    *
 172    */
 173   Result checkSat();
 174
 175   /**
 176    * Get the value of a boolean variable.
 177    *
 178    * @return mkConst<true>, mkConst<false>, or Node::null() if
 179    * unassigned.
 180    */
 181   Node getValue(TNode node) const;
 182
 183   /**
 184    * Return true if node has an associated SAT literal.
 185    */
 186   bool isSatLiteral(TNode node) const;
 187
 188   /**
 189    * Check if the node has a value and return it if yes.
 190    */
 191   bool hasValue(TNode node, bool& value) const;
 192
 193   /**
 194    * Returns the Boolean variables known to the SAT solver.
 195    */
 196   void getBooleanVariables(std::vector<TNode>& outputVariables) const;
 197
 198   /**
 199    * Ensure that the given node will have a designated SAT literal
 200    * that is definitionally equal to it. Note that theory preprocessing is
 201    * applied to n. The node returned by this method can be subsequently queried
 202    * via getSatValue().
 203    */
 204   Node ensureLiteral(TNode n);
 205   /**
 206    * This returns the theory-preprocessed form of term n. This rewrites and
 207    * preprocesses n, which notice may involve adding clauses to the SAT solver
 208    * if preprocessing n involves introducing new skolems.
 209    */
 210   Node getPreprocessedTerm(TNode n);
 211   /**
 212    * Same as above, but also compute the skolems in n and in the lemmas
 213    * corresponding to their definition.
 214    *
 215    * Note this will include skolems that occur in the definition lemma
 216    * for all skolems in sks. This is run until a fixed point is reached.
 217    * For example, if k1 has definition (ite A (= k1 k2) (= k1 x)) where k2 is
 218    * another skolem introduced by term formula removal, then calling this
 219    * method on (P k1) will include both k1 and k2 in sks, and their definitions
 220    * in skAsserts.
 221    */
 222   Node getPreprocessedTerm(TNode n,
 223                            std::vector<Node>& skAsserts,
 224                            std::vector<Node>& sks);
 225
 226   /**
 227    * Push the context level.
 228    */
 229   void push();
 230
 231   /**
 232    * Pop the context level.
 233    */
 234   void pop();
 235
 236   /*
 237    * Reset the decisions in the DPLL(T) SAT solver at the current assertion
 238    * level.
 239    */
 240   void resetTrail();
 241
 242   /**
 243    * Get the assertion level of the SAT solver.
 244    */
 245   unsigned getAssertionLevel() const;
 246
 247   /**
 248    * Return true if we are currently searching (either in this or
 249    * another thread).
 250    */
 251   bool isRunning() const;
 252
 253   /**
 254    * Interrupt a running solver (cause a timeout).
 255    *
 256    * Can potentially throw a ModalException.
 257    */
 258   void interrupt();
 259
 260   /**
 261    * Informs the ResourceManager that a resource has been spent.  If out of
 262    * resources, can throw an UnsafeInterruptException exception.
 263    */
 264   void spendResource(ResourceManager::Resource r);
 265
 266   /**
 267    * For debugging.  Return true if "expl" is a well-formed
 268    * explanation for "node," meaning:
 269    *
 270    * 1. expl is either a SAT literal or an AND of SAT literals
 271    *    currently assigned true;
 272    * 2. node is assigned true;
 273    * 3. node does not appear in expl; and
 274    * 4. node was assigned after all of the literals in expl
 275    */
 276   bool properExplanation(TNode node, TNode expl) const;
 277
 278   /** Retrieve this modules proof CNF stream. */
 279   ProofCnfStream* getProofCnfStream();
 280
 281   /** Checks that the proof is closed w.r.t. asserted formulas to this engine as
 282    * well as to the given assertions. */
 283   void checkProof(context::CDList<Node>* assertions);
 284
 285   /**
 286    * Return the prop engine proof. This should be called only when proofs are
 287    * enabled. Returns a proof of false whose free assumptions are the
 288    * preprocessed assertions.
 289    */
 290   std::shared_ptr<ProofNode> getProof();
 291
 292   /** Is proof enabled? */
 293   bool isProofEnabled() const;
 294  private:
 295   /** Dump out the satisfying assignment (after SAT result) */
 296   void printSatisfyingAssignment();
 297
 298   /**
 299    * Converts the given formula to CNF and asserts the CNF to the SAT solver.
 300    * The formula can be removed by the SAT solver after backtracking lower
 301    * than the (SAT and SMT) level at which it was asserted.
 302    *
 303    * @param trn the trust node storing the formula to assert
 304    * @param removable whether this lemma can be quietly removed based
 305    * on an activity heuristic
 306    */
 307   void assertLemmaInternal(theory::TrustNode trn, bool removable);
 308
 309   /**
 310    * Indicates that the SAT solver is currently solving something and we should
 311    * not mess with it's internal state.
 312    */
 313   bool d_inCheckSat;
 314
 315   /** The theory engine we will be using */
 316   TheoryEngine* d_theoryEngine;
 317
 318   /** The decision engine we will be using */
 319   std::unique_ptr<DecisionEngine> d_decisionEngine;
 320
 321   /** The context */
 322   context::Context* d_context;
 323
 324   /** SAT solver's proxy back to theories; kept around for dtor cleanup */
 325   TheoryProxy* d_theoryProxy;
 326
 327   /** The SAT solver proxy */
 328   CDCLTSatSolverInterface* d_satSolver;
 329
 330   /** List of all of the assertions that need to be made */
 331   std::vector<Node> d_assertionList;
 332
 333   /** A pointer to the proof node maneger to be used by this engine. */
 334   ProofNodeManager* d_pnm;
 335
 336   /** The CNF converter in use */
 337   CnfStream* d_cnfStream;
 338   /** Proof-producing CNF converter */
 339   std::unique_ptr<ProofCnfStream> d_pfCnfStream;
 340
 341   /** The proof manager for prop engine */
 342   std::unique_ptr<PropPfManager> d_ppm;
 343
 344   /** Whether we were just interrupted (or not) */
 345   bool d_interrupted;
 346   /** Pointer to resource manager for associated SmtEngine */
 347   ResourceManager* d_resourceManager;
 348
 349   /** Reference to the output manager of the smt engine */
 350   OutputManager& d_outMgr;
 351 };
 352
 353 }  // namespace prop
 354 }  // namespace CVC4
 355
 356 #endif /* CVC4__PROP_ENGINE_H */