logical

package
v1.2.23 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jul 22, 2026 License: Apache-2.0 Imports: 9 Imported by: 0

Documentation

Overview

Copyright Consensys Software Inc.

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

SPDX-License-Identifier: Apache-2.0

Copyright Consensys Software Inc.

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

SPDX-License-Identifier: Apache-2.0

Copyright Consensys Software Inc.

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

SPDX-License-Identifier: Apache-2.0

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

This section is empty.

Types

type Atom 

type Atom[I any, A any] interface {
	array.Comparable[A]
	// Return the logical negation of this atom
	Negate() A
	// Check whether this atom is equivalent to logical truth or falsehood.
	Is(bool) bool
	// CloseOver this term and another, producing a potentially updated version
	// of this term.  For example, closing over "x=y" and "y=0" might given
	// "x=0", etc.
	CloseOver(o A) A
	// String returns a human-readable representation
	String(func(I) string) string
}

Atom represents an indivisible part of a proposition.

type Conjunction 

type Conjunction[I any, A Atom[I, A]] struct {
	// contains filtered or unexported fields
}

Conjunction represents the conjunction of zero or more atoms.

func (Conjunction[I, A]) Atoms 

func (p Conjunction[I, A]) Atoms() []A

Atoms returns the underlying atoms which are conjuncted together.

func (Conjunction[I, A]) Cmp 

func (p Conjunction[I, A]) Cmp(o Conjunction[I, A]) int

Cmp implementation for Comparable interface

func (Conjunction[I, A]) Implies 

func (p Conjunction[I, A]) Implies(other Conjunction[I, A]) bool

Implies checks whether this conjunction implies another. For example, A implies (A B), whilst (A B) implies (A B C), etc.

func (Conjunction[I, A]) Remove 

func (p Conjunction[I, A]) Remove(atom A) (Conjunction[I, A], bool)

Remove an atom from this conjunction (if it is contained within), or simply return this conjunction.

func (Conjunction[I, A]) String 

func (p Conjunction[I, A]) String(braces bool, mapping func(I) string) string

type Equality 

type Equality[I Variable[I]] struct {
	// Sign indicates whether this is an Equality (==) or a non-Equality (!=).
	Sign bool
	// Left variable
	Left I
	// Right variable or constant
	Right util.Union[I, big.Int]
}

Equality represents a fundamental atom which is either an Equality (=) or a non-Equality (≠) between a variable and either a variable or a constant.

func Equals 

func Equals[I Variable[I]](l I, r I) Equality[I]

Equals returns an equality over two variables (i.e. l = r)

func EqualsConst 

func EqualsConst[I Variable[I]](l I, r big.Int) Equality[I]

EqualsConst returns an equality over a variable and a constant

func NotEquals 

func NotEquals[I Variable[I]](l I, r I) Equality[I]

NotEquals returns a non-Equality over two variables (i.e. l ≠ r)

func NotEqualsConst 

func NotEqualsConst[I Variable[I]](l I, r big.Int) Equality[I]

NotEqualsConst returns an equality over a variable and a constant

func (Equality[I]) CloseOver 

func (p Equality[I]) CloseOver(o Equality[I]) Equality[I]

CloseOver implementation for Atom interface

func (Equality[I]) Cmp 

func (p Equality[I]) Cmp(o Equality[I]) int

Cmp implementation for Comparable interface

func (Equality[I]) Is 

func (p Equality[I]) Is(truth bool) bool

Is implementation of Atom interface

func (Equality[I]) Negate 

func (p Equality[I]) Negate() Equality[I]

Negate this Equality (i.e. turn it from "==" to "!=" or vice-versa)

func (Equality[I]) String 

func (p Equality[I]) String(mapping func(I) string) string

type Equation 

type Equation[S util.Comparable[S], T poly.Term[S, T], P poly.Polynomial[S, T, P]] struct {
	// contains filtered or unexported fields
}

Equation represents an equation between two polynomials, such as "0 == x + 1" or "0 != 2xy + 3", etc.

func Vanishes 

func Vanishes[S util.Comparable[S], T poly.Term[S, T], P poly.Polynomial[S, T, P]](term P) Equation[S, T, P]

Vanishes constraints a new vanishing constraint (P == 0) for a given term P.

func (Equation[S, T, P]) CloseOver 

func (p Equation[S, T, P]) CloseOver(o Equation[S, T, P]) Equation[S, T, P]

CloseOver implementation for Atom interface

func (Equation[S, T, P]) Cmp 

func (p Equation[S, T, P]) Cmp(o Equation[S, T, P]) int

Cmp implementation for Comparable interface

func (Equation[S, T, P]) Is 

func (p Equation[S, T, P]) Is(truth bool) bool

Is implementation of Atom interface

func (Equation[S, T, P]) LeftHandSide 

func (p Equation[S, T, P]) LeftHandSide() P

LeftHandSide returns the left-hand side of this equation

func (Equation[S, T, P]) Negate 

func (p Equation[S, T, P]) Negate() Equation[S, T, P]

Negate this Equality (i.e. turn it from "==" to "!=" or vice-versa)

func (Equation[S, T, P]) RightHandSide 

func (p Equation[S, T, P]) RightHandSide() P

RightHandSide returns the right-hand side of this equation

func (Equation[S, T, P]) Sign 

func (p Equation[S, T, P]) Sign() bool

Sign returns the sign of this atom (either positive for equality or negative for non-equality).

func (Equation[S, T, P]) String 

func (p Equation[S, T, P]) String(mapping func(S) string) string

type Proposition 

type Proposition[I any, A Atom[I, A]] struct {
	// contains filtered or unexported fields
}

Proposition provides an abstraction over logical statements made up from conjunctions and disjunctions of atoms (i.e. atomic formulae). Currently, propositions are always stored in Disjunctive Normal Form (DNF).

func NewProposition 

func NewProposition[I any, A Atom[I, A]](atom A) Proposition[I, A]

NewProposition constructs a proposition from a single atom.

func Truth 

func Truth[I any, A Atom[I, A]](val bool) Proposition[I, A]

Truth constructs either logical truth or logical false

func (*Proposition[I, A]) And 

func (p *Proposition[I, A]) And(other Proposition[I, A]) Proposition[I, A]

And returns the conjunction of two propositions.

func (*Proposition[I, A]) Clone 

func (p *Proposition[I, A]) Clone() Proposition[I, A]

Clone this proposition making sure the resulting tree is disjoint

func (*Proposition[I, A]) Conjuncts 

func (p *Proposition[I, A]) Conjuncts() []Conjunction[I, A]

Conjuncts returns the individual conjunctions which form this proposition.

func (*Proposition[I, A]) Equals 

func (p *Proposition[I, A]) Equals(other Proposition[I, A]) bool

Equals returns true if the two propositions are identical.

func (*Proposition[I, A]) IsFalse 

func (p *Proposition[I, A]) IsFalse() bool

IsFalse checks whether or not this branch corresponds with logical false or not.

func (*Proposition[I, A]) IsTrue 

func (p *Proposition[I, A]) IsTrue() bool

IsTrue checks whether or not this branch corresponds with logical truth or not.

func (*Proposition[I, A]) Negate 

func (p *Proposition[I, A]) Negate() Proposition[I, A]

Negate returns the logical negation of this proposition.

func (*Proposition[I, A]) Or 

func (p *Proposition[I, A]) Or(other Proposition[I, A]) Proposition[I, A]

Or returns the disjunction of two propositions.

func (*Proposition[I, A]) String 

func (p *Proposition[I, A]) String(mapping func(I) string) string

type Variable 

type Variable[I any] interface {
	fmt.Stringer
	array.Comparable[I]
}

Variable defines some required characteristics of any variable identifier suitable for use within an equality.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.