Class: PropLogic::DefaultIncrementalSolver

Inherits:
Object
  • Object
show all
Defined in:
lib/prop_logic/default_incremental_solver.rb

Overview

Default implementation of incremental SAT solver. Provided for reference implementation and avoiding non-existent error. (Using normal solver, not incrementally)

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(term) ⇒ DefaultIncrementalSolver

Returns a new instance of DefaultIncrementalSolver.

Parameters:

  • initial (Term) —

    term



9
10
11
 
# File 'lib/prop_logic/default_incremental_solver.rb', line 9

def initialize(term)
  @term = term
end

Instance Attribute Details

#term ⇒ Object (readonly)

Current term



14
15
16
 
# File 'lib/prop_logic/default_incremental_solver.rb', line 14

def term
  @term
end

Instance Method Details

#add(*terms) ⇒ DefaultIncrementalSolver Also known as: <<

Adding new terms to this solver.

Parameters:

  • terms (Term) —

    to add.

Returns:



19
20
21
22
 
# File 'lib/prop_logic/default_incremental_solver.rb', line 19

def add(*terms)
  @term = @term.and(*terms)
  self
end

#sat? ⇒ Term, false

Check satisfiability of terms.

Returns:

  • (Term) —

    if satisfied

  • (false) —

    if unsatisfied



29
30
31
 
# File 'lib/prop_logic/default_incremental_solver.rb', line 29

def sat?
  @term.sat?
end