README

ocaml-logicalform

LogicalForm provides modules for efficient and intuitive manipulation of logical expressions withinOCaml.

OPAM Package  · API Documentation   |  Installation  · Usage  · Change Log  · License (MIT)

Installation

The library is released asocaml-logicalform package, and is available onopam.

Stable version

$ opam install ocaml-logicalform

Development version (pinned to this repository)

$ opam pin add ocaml-logicalform https://github.com/SaswatPadhi/ocaml-logicalform.git$ opam install ocaml-logicalform

Usage

We assume the following environment for the examples below:

open LogicalForm.Std (* Predefined standard forms *)open Sexplib         (* Translating to/from S-Expressions *)

Creating Expressions

Using constructors

We use integer indices (starting at1) for variables appearing in literals:

• `Pos x creates anunchecked positive literal

• `Neg x creates anunchecked negative literal

• `L?? x or`L (id x) validatesx:

  • creates a positive literal forx-th variable ifx > 0

  • creates a negative literal forx-th variable ifx < 0

  • throws an exception ifx = 0

They are combined using`And and`Or constructors to form bigger expressions, as shown below:

(* Various representations for E = ~(x1 /\ (x2 \/ (x3 /\ ~x4))) *)(* E in conjunctive normal form (CNF) : unchecked literals *)let cnf : CNF.t =  `And [ `Or [ `Neg 1 ; `Neg 2 ]       ; `Or [ `Neg 1 ; `Neg 3 ; `Pos 4 ]](* E in disjunctive normal form (DNF) : unchecked literals *)let dnf : DNF.t =  `Or [ `Neg 1      ; `And [ `Neg 2 ; `Neg 3 ]      ; `And [ `Neg 2 ; `Pos 4 ]      ](* E in negation normal form (NNF) : literals validated *)let nnf : NNF.t =  `Or [ `L?? (-1)      ; `And [ `L?? (-2)             ; `Or [ `L?? (-3) ; `L?? 4 ]             ]      ](* E not in normal form  : literals validated *)let unnf : UnNF.t =  `Not ( `And [ `L (id 1)              ; `Or [ `L (id 2)                    ; `And [ `L (id 3) ; `L (id (-4)) ]                    ]              ])

From S-Expressions

One can also parseLogicalForm expressions fromSMT-LIB styleS-Expressions:

let cnf' : CNF.t =  CNF.of_pretty_sexp (    Sexp.of_string "(and (or (not x1) (not x2)) (or (not x1) (not x3) x4))")

Thecnf' expression should be equivalent tocnf:

(* Since cnf used `Pos and `Neg, we must validate it *)# cnf' = CNF.validate cnf;;- : bool = true

LogicalForm also supports custom prefixes for variables (instead of thex as above), and custom operator names for conjunction, disjunction, and negation. (Seeadvanced usage).

Pretty Printing

Compact human readable strings

# DNF.to_pretty_string dnf;;- : string = "(~x1 | (~x2 & ~x3) | (~x2 & x4))"# NNF.to_pretty_string nnf;;- : string = "(~x1 | (~x2 & (~x3 | x4)))"

S-Expressions

# Sexp.to_string_hum (CNF.to_pretty_sexp cnf);;- : string = "(and (or (not x1) (not x2)) (or (not x1) (not x3) x4))"# Sexp.to_string_hum (UnNF.to_pretty_sexp unnf);;- : string = "(not (and x1 (or x2 (and x3 (not x4)))))"

CNF andDNF can be interpreted asNNF expressions, but not vice versa. Similarly an expression in any normal form can be interpreted as anUnNF expression, but not vice versa.

# NNF.to_pretty_string (cnf :> NNF.t);;- : string = "((~x1 | ~x2) & (~x1 | ~x3 | x4))"# CNF.to_pretty_string (nnf :> CNF.t);;Error: ...# Sexp.to_string_hum (UnNF.to_pretty_sexp (nnf :> UnNF.t));;- : string = "(or (not x1) (and (not x2) (or (not x3) x4)))"# NNF.to_pretty_string (unnf :> NNF.t);;Error: ...

Extracting Executable Functions

# let cnf_f = CNF.eval cnf;;val cnf_f : bool array -> bool option = <fun>

An executable function for aLogicalForm expression consumes anarray ofbool values, and returns:

• None if the execution failed, because the value of a literal was not provided

• Some b if the expression evaluates to thebool valueb

(* Not enough data to evaluate *)# cnf_f [| true |];;- : bool option = None(* Short-circuited evaluation *)# cnf_f [| false |];;- : bool option = Some true(* Unused variables are ignored *)# cnf_f [| true ; false ; false ; true ; false ; true |];;- : bool option = Some true

Combining Expressions

Every formF inLogicalForm is,

• Conjunctable: supports conjunction of alist ofF expressions usingand_

• Disjunctable: supports conjunction of alist ofF expressions usingor_

• Negatable: allows negation of anF expression usingnot_

Let us define two new expressions:

let cnf_2 : CNF.t = `And [ `Pos 1 ; `Or [ `Neg 2 ; `Pos 3 ] ]let dnf_2 : DNF.t = `Or [ `Pos 3 ; `And [ `Pos 2 ; `Neg 1 ] ; `Pos 4 ]

We can now combine:

(* Disjunction of CNFs into a CNF *)# let cnf_3 = CNF.or_ [ cnf ; cnf_2 ];;val cnf_3 : CNF.t = ...(* Conjunction of expressions in arbitrary NFs into an NNF *)# let nnf_2 = NNF.and_ [ (dnf :> NNF.t) ; nnf ; (cnf :> NNF.t) ];;val nnf_2 : NNF.t = ...

Advanced Usage

Printing and parsing options

Users may override default pretty-printing styles for strings and S-Expressions as below:

(* to_pretty_string uses infix operators *)let my_infix_style = {  PPStyle.Infix.default  with var_prefix = "j"     ; _or_ = " OR "     ; _and_ = " AND "}(* to_pretty_sexp uses prefix operators *)let my_prefix_style = {  PPStyle.Prefix.default  with var_prefix = "k"     ; or_ = "O"     ; and_ = "A"     ; not_ = "N"}

These styles may be provided to the pretty-printing functions as shown below:

# NNF.to_pretty_string nnf ~style:my_infix_style;;- : string = "(~j1 OR (~j2 AND (~j3 OR j4)))"# nnf = NNF.of_pretty_sexp          ~style:my_prefix_style          (Sexp.of_string "(O (N k1) (A (N k2) (O (N k3) k4)))")- : bool = true

Literal index type

LogicalForm allows literals to contain custom data types. TheStd modules provides pre-definedCNF,DNF,NNF, andUnNF modules based onBase.Int type. On modern 64-bit machines, one may restrict the index type toBase.Int32 (instead ofBase.Int = Base.Int64):

module Index32 = LogicalForm.Index.Make(Base.Int32)let ( ?? ) = Index32.idmodule Literal32 = LogicalForm.Literal.Make(Index32)module Clause32 = LogicalForm.Clause.Make(Literal32)module CNF32 = LogicalForm.CNF.Make(Clause32)module NNF32 = LogicalForm.NNF.Make(Literal32)...

All examples shown above should work for these 32-bit modules too.

License(MIT)

Copyright © 2018 Saswat Padhi

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

1. ocaml-migrate-parsetree< "2.0.0"
2. base>= "v0.9" & < "v0.14"
3. ppx_sexp_conv>= "v0.9" & < "v0.14"
4. jbuilder>= "1.0+beta10"
5. ocaml>= "4.04.0"

1. odocwith-doc

None

None