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>
Go to the source code of this file.
Classes
- class lastToFirst_lt
- struct reduceDB_lt
Variables
- const bool defer_theory_propagation = true
- const bool eager_explanation = true
- const bool keep_lazy_explanation = true
- const bool push_theory_propagation = true
- const bool push_theory_implication = true
- const bool push_theory_clause = true
- const vector< Var >::size_type prop_lookahead = 1
- const bool protocol = false
- const bool debug_full = false
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 |
| const bool push_theory_implication = true |
| const bool push_theory_clause = true |
| const vector<Var>::size_type prop_lookahead = 1 |
| const bool protocol = false |
Definition at line 105 of file minisat_solver.cpp.
Referenced by MiniSat::Solver::protocolPropagation(), MiniSat::Solver::push(), and MiniSat::Solver::search().
| const bool debug_full = false |
Definition at line 112 of file minisat_solver.cpp.
Referenced by MiniSat::Solver::allClausesSatisfied(), MiniSat::Solver::checkClauses(), MiniSat::Solver::checkTrail(), and MiniSat::Solver::checkWatched().
