CVC3
Classes | Variables
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
 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
const bool debug_full = false