Crate liquid_fixpoint 

This crate implements an interface to the liquid-fixpoint binary

Modules

constraint 🔒

constraint_with_env 🔒

format 🔒

graph 🔒

parser

sexp

smt_fmt 🔒

Shared SMTLIB serialization methods

smt_horn

suggestion_solver 🔒

Validity check + Quantifier Elimination. Used to make suggestions.

z3_subprocess 🔒

Subprocess for interfacing with Z3. We only added enough features to support [suggustion_solver.rs]

Macros

declare_types

Structs

Axiom

A fact that is asserted to the SMT solver, universally quantified over args.

Bind

ConstDecl

CrashInfo

DataCtor

DataDecl

DataField

Error

ErrorInner 🔒

FlatConstraint

FunBody

FunDef

FunSort

KVarBind

KVarDecl

QualParam

Qualifier

SortDecl

Stats

SuggestionSolver

Task

VerificationResult

WKVar

Enums

BinOp

BinRel

Constant

Constraint

Expr

FixpointError

An error that prevented fixpoint from producing a result

FixpointStatus

LeanStatus

Pred

Quantifier

SmtSolver

Sort

SortCtor

SuggestionSolverError

ThyFunc

Traits

FixpointFmt

Identifier

Types

Functions

check_validity

qe_and_simplify

Type Aliases

Assignments

Type alias for qualifier assignments used in constraint solving