liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Solver.Interpreter

Description

This module is a preliminary part of the implementation of "Proof by Logical Evaluation" where we unfold function definitions if they *must* be unfolded, to strengthen the environments with function-definition-equalities.

In this module, we attempt to verify as many of the PLE constaints as possible without invoking the SMT solver or performing any I/O at all. To this end, we use an interpreter in Haskell to attempt to evaluate down expressions and generate equalities.

Synopsis

Documentation

instInterpreter :: Loc a => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a) Source #

Strengthen Constraint Environments via PLE

data ICtx Source #

ICtx is the local information -- at each trie node -- obtained by incremental PLE

Constructors

ICtx 

Fields

data Knowledge Source #

Knowledge (SMT Interaction)

Constructors

KN 

Fields

class Simplifiable a where Source #

Methods

simplify :: Knowledge -> ICtx -> a -> a Source #

Instances

Instances details
Simplifiable Expr Source # 
Instance details

Defined in Language.Fixpoint.Solver.Interpreter

Methods

simplify :: Knowledge -> ICtx -> Expr -> Expr Source #

interpret :: ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr Source #