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

• class lastToFirst_lt
• struct reduceDB_lt

Functions

• bool MiniSat::cvcToMiniSat (const SAT::Clause &clause, std::vector< Lit > &literals)

Variables

• const bool defer_theory_propagation = true
• const bool eager_explanation = true

  theory implications
  

• const bool keep_lazy_explanation = true
• const bool push_theory_propagation = true

  pushes
  

• 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

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

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().

---