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
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