View GitHub Repository prop_logic

Schedule Inspection
Subscribe

DefaultIncrementalSolver   A
last analyzed

↳ Parent: Project

Complexity

Total Complexity 3

Size/Duplication

Total Lines 26
Duplicated Lines 0 %
Metric Value
dl 0
loc 26
rs 10
wmc 3

3 Methods

Rating   Name   Duplication   Size   Complexity  
A sat? 0 3 1
A add() 0 4 1
A initialize() 0 3 1
1 
module PropLogic
2 
  #
3 
  # Default implementation of incremental SAT solver.
4 
  # Provided for reference implementation and avoiding non-existent error.
5 
  # (Using normal solver, not incrementally)
6 
  #
7 
  class DefaultIncrementalSolver
8 
    # @param [Term] initial term
9 
    def initialize(term)
10 
      @term = term
11 
    end
12 

            


            
                                                                        
                            
            
                                    
            
            

                
                    13
                

                                    
                                                    
                
                
                
    # Current term

            


            
                                                                        
                            
            
                                    
            
            

                
                    14
                

                                    
                                                    
                
                
                
    attr_reader :term

            


            
                                                                        
                            
            
                                    
            
            

                
                    15
                

                                    
                                                    
                
                
                

            


            
                                                                        
                            
            
                                    
            
            

                
                    16
                

                                    
                                                    
                
                
                
    # Adding new terms to this solver.

            


            
                                                                        
                            
            
                                    
            
            

                
                    17
                

                                    
                                                    
                
                
                
    # @param [Term] terms to add.

            


            
                                                                        
                            
            
                                    
            
            

                
                    18
                

                                    
                                                    
                
                
                
    # @return [DefaultIncrementalSolver] self

            


            
                                                                        
                            
            
                                    
            
            

                
                    19
                

                                    
                                                    
                
                
                
    def add(*terms)

            


            
                                                                        
                            
            
                                    
            
            

                
                    20
                

                                    
                                                    
                
                
                
      @term = @term.and(*terms)

            


            
                                                                        
                            
            
                                    
            
            

                
                    21
                

                                    
                                                    
                
                
                
      self

            


            
                                                                        
                            
            
                                    
            
            

                
                    22
                

                                    
                                                    
                
                
                
    end

            


            
                                                                        
                            
            
                                    
            
            

                
                    23
                

                                    
                                                    
                
                
                

            


            
                                                                        
                            
            
                                    
            
            

                
                    24
                

                                    
                                                    
                
                
                
    alias_method :<<, :add

            


            
                                                                        
                            
            
                                    
            
            

                
                    25
                

                                    
                                                    
                
                
                

            


            
                                                                        
                            
            
                                    
            
            

                
                    26
                

                                    
                                                    
                
                
                
    # Check satisfiability of terms.

            


            
                                                                        
                            
            
                                    
            
            

                
                    27
                

                                    
                                                    
                
                
                
    # @return [Term] if satisfied

            


            
                                                                        
                            
            
                                    
            
            

                
                    28
                

                                    
                                                    
                
                
                
    # @return [false] if unsatisfied

            


            
                                                                        
                            
            
                                    
            
            

                
                    29
                

                                    
                                                    
                
                
                
    def sat?

            


            
                                                                        
                            
            
                                    
            
            

                
                    30
                

                                    
                                                    
                
                
                
      @term.sat?

            


            
                                                                        
                            
            
                                    
            
            

                
                    31
                

                                    
                                                    
                
                
                
    end

            


            
                                                                                                            
                            
            
                                    
            
            

                
                    32
                

                                    
                                                    
                
                
                
  end

            


            
                                                                                                            
                                                                
            
                                    
            
            

                
                    33
                

                                    
                                                    
                
                
                
end

            


            
                                                        
            
                                    
            
            

                
                    34