This file is indexed.

/usr/include/cvc3/dpllt.h is in libcvc3-dev 2.4.1-5.1ubuntu1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
/*****************************************************************************/
/*!
 *\file dpllt.h
 *\brief Generic DPLL(T) module
 *
 * Author: Clark Barrett
 *
 * Created: Mon Dec 12 16:28:08 2005
 */
/*****************************************************************************/

#ifndef _cvc3__include__dpllt_h_
#define _cvc3__include__dpllt_h_

#include "queryresult.h"
#include "cnf.h"
#include "cnf_manager.h"
#include "proof.h" 
#include "theory_core.h"

namespace SAT {

class DPLLT {
public:

  enum ConsistentResult {INCONSISTENT, MAYBE_CONSISTENT, CONSISTENT };

  class TheoryAPI {
  public:
    TheoryAPI() {}
    virtual ~TheoryAPI() {}

    //! Set a checkpoint for backtracking
    virtual void push() = 0;
    //! Restore most recent checkpoint
    virtual void pop() = 0;

    //! Notify theory when a literal is set to true
    virtual void assertLit(Lit l) = 0;

    //! Check consistency of the current assignment.
    /*! The result is either INCONSISTENT, MAYBE_CONSISTENT, or CONSISTENT
     * Most of the time, fullEffort should be false, and the result will most
     * likely be either INCONSISTENT or MAYBE_CONSISTENT.  To force a full
     * check, set fullEffort to true.  When fullEffort is set to true, the
     * only way the result can be MAYBE_CONSISTENT is if there are new clauses
     * to get (via getNewClauses).
     * \param cnf should be empty initially.  If INCONSISTENT is returned,
     * then cnf will contain one or more clauses ruling out the current
     * assignment when it returns.  Otherwise, cnf is unchanged.
     * \param fullEffort true for a full check, false for a fast check
     */
    virtual ConsistentResult checkConsistent(CNF_Formula& cnf, bool fullEffort) = 0;


    //! Check if the work budget has been exceeded
    /*! If true, it means that the engine should quit and return ABORT.
     * Otherwise, it should proceed normally.  This should be checked regularly.
     */
    virtual bool outOfResources() = 0;

    //! Get a literal that is implied by the current assignment.
    /*! This is theory propagation.  It can be called repeatedly and returns a
     * Null literal when there are no more literals to propagate.  It should
     * only be called when the assignment is not known to be inconsistent.
     */
    virtual Lit getImplication() = 0;

    //! Get an explanation for a literal that was implied
    /*! Given a literal l that is true in the current assignment as a result of
     * an earlier call to getImplication(), this method returns a set of clauses which
     * justifies the propagation of that literal.  The clauses will contain the
     * literal l as well as other literals that are in the current assignment.
     * The clauses are such that they would have propagated l via unit
     * propagation at the time getImplication() was called.
     * \param l the literal
     * \param c should be empty initially. */
    virtual void getExplanation(Lit l, CNF_Formula& c) = 0;

    //! Get new clauses from the theory.
    /*! This is extended theory learning.  Returns false if there are no new
     * clauses to get.  Otherwise, returns true and new clauses are added to
     * cnf.  Note that the new clauses (if any) are theory lemmas, i.e. clauses
     * that are valid in the theory and not dependent on the current
     * assignment.  The clauses may contain new literals as well as literals
     * that are true in the current assignment.
     * \param cnf should be empty initially. */
    virtual bool getNewClauses(CNF_Formula& cnf) = 0;

  };

  class Decider {
  public:
    Decider() {}
    virtual ~Decider() {}

    //! Make a decision.
    /* Returns a NULL Lit if there are no more decisions to make */
    virtual Lit makeDecision() = 0;

  };

protected:
  TheoryAPI* d_theoryAPI;
  Decider* d_decider;

public:
  //! Constructor
  /*! The client constructing DPLLT must provide an implementation of
   * TheoryAPI.  It may also optionally provide an implementation of Decider.
   * If decider is NULL, then the DPLLT class must make its own decisions.
   */
  DPLLT(TheoryAPI* theoryAPI, Decider* decider)
    : d_theoryAPI(theoryAPI), d_decider(decider) {}
  virtual ~DPLLT() {}

  TheoryAPI* theoryAPI() { return d_theoryAPI; }
  Decider* decider() { return d_decider; }

  void setDecider(Decider* decider) { d_decider = decider; }

  //! Set a checkpoint for backtracking
  /*! This should effectively save the current state of the solver.  Note that
   * it should also result in a call to TheoryAPI::push.
   */
  virtual void push() = 0;

  //! Restore checkpoint
  /*! This should return the state to what it was immediately before the last
   * call to push.  In particular, if one or more calls to checkSat,
   * continueCheck, or addAssertion have been made since the last push, these
   * should be undone.  Note also that in this case, a single call to
   * DPLLT::pop may result in multiple calls to TheoryAPI::pop.
   */
  virtual void pop() = 0;

  //! Add new clauses to the SAT solver
  /*! This is used to add clauses that form a "context" for the next call to
   * checkSat
   */
  virtual void addAssertion(const CNF_Formula& cnf) = 0;

  virtual std::vector<SAT::Lit> getCurAssignments() =0 ;
  virtual std::vector<std::vector<SAT::Lit> > getCurClauses() =0 ;

  //! Check the satisfiability of a set of clauses in the current context
  /*! If the result is SATISFIABLE, UNKNOWN, or ABORT, the DPLLT engine should
   * remain in the state it is in until pop() is called.  If the result is
   * UNSATISFIABLE, the DPLLT engine should return to the state it was in when
   * called.  Note that it should be possible to call checkSat multiple times,
   * even if the result is true (each additional call should use the context
   * left by the previous call).
   */
  virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf) = 0;

  //! Continue checking the last check with additional constraints
  /*! Should only be called after a previous call to checkSat (or
   * continueCheck) that returned SATISFIABLE.  It should add the clauses in
   * cnf to the existing clause database and search for a satisfying
   * assignment.  As with checkSat, if the result is not UNSATISFIABLE, the
   * DPLLT engine should remain in the state containing the satisfiable
   * assignment until pop() is called.  Similarly, if the result is
   * UNSATISFIABLE, the DPLLT engine should return to the state it was in when
   * checkSat was last called.
   */
  virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf) = 0;

  //! Get value of variable: unassigned, false, or true
  virtual Var::Val getValue(Var v) = 0;

  //! Get the proof from SAT engine. 
  virtual CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) = 0 ; 

};

}

#endif