class PropLogic::Minisat::IncrementalSolver

Incremental solver using minisat. @note currently only Ruby part is incremental.

Public Class Methods

new(initial_term) click to toggle source

constructor. @param [Term] initial term for starting SAT solver.

# File lib/prop_logic/minisat/incremental_solver.rb, line 13
def initialize(initial_term)
  @solver = ::MiniSat::Solver.new
  # automagically add variable in Hash
  @variables_map = Hash.new { |h, k| h[k] = @solver.new_var }
  @terms = []
  @variables = []
  # true if False was added
  @contradicted = false
  add initial_term
end

Public Instance Methods

<<(*terms)
Alias for: add
add(*terms) click to toggle source

add terms to this solver. @return [IncrementalSolver] returns self

# File lib/prop_logic/minisat/incremental_solver.rb, line 37
def add(*terms)
  terms.each { |term| add_one_term term }
  self
end
Also aliased as: <<
sat?() click to toggle source

check if terms are satisfiable. @return [Term] term satisfying conditions. @return [false] if unsatisfied.

# File lib/prop_logic/minisat/incremental_solver.rb, line 47
def sat?
  return false if @contradicted
  return True if variables.empty?
  vars = []
  unless @terms.empty?
    return false unless @solver.solve
    ret_vars = variables & @variables_map.keys
    vars = ret_vars.map { |k| @solver[@variables_map[k]] ? k : ~k }
  end
  extra_vars = variables - @variables_map.keys
  PropLogic.all_and(*vars, *extra_vars)
end
term() click to toggle source
# File lib/prop_logic/minisat/incremental_solver.rb, line 29
def term
  return False if @contradicted
  return True if @terms.empty?
  PropLogic.all_and(*@terms)
end
variables() click to toggle source

@return [Array] containing variables

# File lib/prop_logic/minisat/incremental_solver.rb, line 25
def variables
  @variables.dup
end

Private Instance Methods

add_one_term(term) click to toggle source
# File lib/prop_logic/minisat/incremental_solver.rb, line 83
def add_one_term(term)
  @variables |= term.variables
  term = term.to_cnf
  return if term == True
  if term == False
    @contradicted = true
    return
  end
  if term.is_a?(AndTerm)
    term.terms.each { |t| add_or_term t }
  else
    add_or_term term
  end
end
add_or_term(term) click to toggle source
# File lib/prop_logic/minisat/incremental_solver.rb, line 73
def add_or_term(term)
  vars = if term.is_a?(OrTerm)
           term.terms.map { |v| sat_variable v }
         else
           [sat_variable(term)]
         end
  @solver << vars
  @terms << term
end
sat_variable(maybe_inversed_variable) click to toggle source
# File lib/prop_logic/minisat/incremental_solver.rb, line 62
def sat_variable(maybe_inversed_variable)
  case maybe_inversed_variable
  when Variable
    @variables_map[maybe_inversed_variable]
  when NotTerm
    -@variables_map[maybe_inversed_variable.terms[0]]
  else
    raise TypeError
  end
end