minisat_solver.cpp File Reference

Adaptation of MiniSat to DPLL(T). More...

#include "minisat_solver.h"
#include "minisat_types.h"
#include <cmath>
#include <iostream>
#include <algorithm>

Include dependency graph for minisat_solver.cpp:

Go to the source code of this file.

Classes

Variables


Detailed Description

Adaptation of MiniSat to DPLL(T).

Author: Alexander Fuchs

Created: Fri Sep 08 11:04:00 2006


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 LICENSE file provided with this distribution.


Definition in file minisat_solver.cpp.


Variable Documentation

const bool defer_theory_propagation = true

Constants

Definition at line 63 of file minisat_solver.cpp.

Referenced by MiniSat::Solver::propagate(), MiniSat::Solver::push(), and MiniSat::Solver::search().

const bool eager_explanation = true

theory implications

Definition at line 70 of file minisat_solver.cpp.

Referenced by MiniSat::Solver::push(), MiniSat::Solver::resolveTheoryImplication(), and MiniSat::Solver::search().

const bool keep_lazy_explanation = true

Definition at line 76 of file minisat_solver.cpp.

Referenced by MiniSat::Solver::resolveTheoryImplication().

const bool push_theory_propagation = true

pushes

Definition at line 87 of file minisat_solver.cpp.

Referenced by MiniSat::Solver::push().

const bool push_theory_implication = true

Definition at line 91 of file minisat_solver.cpp.

Referenced by MiniSat::Solver::push().

const bool push_theory_clause = true

Definition at line 95 of file minisat_solver.cpp.

Referenced by MiniSat::Solver::push().

const vector<Var>::size_type prop_lookahead = 1

Definition at line 101 of file minisat_solver.cpp.

Referenced by MiniSat::Solver::propLookahead().

const bool protocol = false

const bool debug_full = false


Generated on Thu Oct 15 22:16:55 2009 for CVC3 by  doxygen 1.5.8