/usr/include/cvc3/dpllt_minisat.h is in libcvc3-dev 2.4.1-5ubuntu1.
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 | /*****************************************************************************/
/*!
*\file dpllt_minisat.h
*\brief Implementation of dpllt module based on minisat
*
* Author: Alexander Fuchs
*
* Created: Fri Sep 08 11:04:00 2006
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*/
/*****************************************************************************/
#ifndef _cvc3__sat__dpllt_minisat_h_
#define _cvc3__sat__dpllt_minisat_h_
#include "dpllt.h"
#include "proof.h"
#include "cnf_manager.h"
#include <stack>
// forward declaration of the minisat solver
namespace MiniSat {
class Solver;
}
namespace SAT {
class SatProof;
// an implementation of the DPLLT interface using an adapted MiniSat SAT solver
class DPLLTMiniSat : public DPLLT {
public:
protected:
// determines if the derivation statistic of the solver
// is printed after the derivation terminates.
// can only be set with the constructor
bool d_printStats;
// if true then minisat will create a derivation
// of the empty clause for an unsatisfiable problem.
// see getProof().
bool d_createProof;
// if d_createProof, then the proof of the last unsatisfiable search
SatProof* d_proof;
// the dpllt interface operates in a stack fashion via checkSat and push.
// each stack's data is stored in a level, which is just an instance of MiniSat.
// whenever a checkSat or push is done on a solver that is already in a search,
// a new solver is created and pushed.
std::stack<MiniSat::Solver*> d_solvers;
// returnes the currently active MiniSat instance
//
// must not be called when there is no active MiniSat instance,
// i.e. d_solvers is empty.
MiniSat::Solver* getActiveSolver();
// creates a solver as an extension of the previous solver
// (i.e. takes clauses/assignments/lemmas)
// and pushes it on d_solvers
void pushSolver();
// called by checkSat and continueCheck to initiate a search
// with a SAT solver
CVC3::QueryResult search();
public:
DPLLTMiniSat(TheoryAPI* theoryAPI, Decider* decider,
bool printStats = false, bool createProof = false);
virtual ~DPLLTMiniSat();
// Implementation of the DPLLT interface
virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf);
virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf);
virtual void push();
virtual void pop();
virtual void addAssertion(const CNF_Formula& cnf);
virtual std::vector<SAT::Lit> getCurAssignments() ;
virtual std::vector<std::vector<SAT::Lit> > getCurClauses();
virtual Var::Val getValue(Var v);
// if createProof was given returns a proof of the last unsatisfiable search,
// otherwise (or if there was no unsatisfiable search) NULL
// ownership remains with DPLLTMiniSat
SatProof* getProof() {
DebugAssert((d_proof != NULL), "null proof foound") ;
return d_proof;
};
CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) ;
};
}
#endif
|