yices2

package
Version: v0.0.0-...-52298bf Latest Latest
Warning

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

Go to latest
Published: Jul 2, 2020 License: MIT Imports: 4 Imported by: 0

Documentation

Index

Constants

View Source
const (
	ErrorCtxInvalidOperation ErrorCodeT = 400 + iota
	ErrorCtxOperationNotSupported
	ErrorCtxUnknownDelegate      = 420 + iota // Since 2.6.2.
	ErrorCtxDelegateNotAvailable              // Since 2.6.2.
)

These are the go versions of the yices_types.h error_code (400 < code <= 500 constants: Error codes for other operations.)

Variables

This section is empty.

Functions

func AssertBlockingClause

func AssertBlockingClause(ctx ContextT) int32

AssertBlockingClause is the go version of yices_assert_blocking_clause.

func AssertFormula

func AssertFormula(ctx ContextT, t TermT) int32

AssertFormula is the go version of yices_assert_formula.

func AssertFormulas

func AssertFormulas(ctx ContextT, t []TermT) int32

AssertFormulas is the go version of yices_assert_formulas.

func BoolConstValue

func BoolConstValue(t TermT, val *int32) int32

BoolConstValue is the go version of yices_bool_const_value.

func BuildArch

func BuildArch() string

BuildArch is the yices2 library build architecture.

func BuildDate

func BuildDate() string

BuildDate is the yices2 library build date.

func BuildMode

func BuildMode() string

BuildMode is the yices2 library build mode.

func BvConstValue

func BvConstValue(t TermT, val []int32) int32

BvConstValue is the go version of yices_bv_const_value.

func BvsumComponent

func BvsumComponent(t TermT, i int32, val []int32, term *TermT) int32

BvsumComponent is the go version of yices_bvsum_component.

func BvtypeSize

func BvtypeSize(tau TypeT) uint32

BvtypeSize is the go version of yices_bvtype_size.

func ClearError

func ClearError()

ClearError reset the current yices error struct.

func ClearTermName

func ClearTermName(t TermT) int32

ClearTermName is the go version of yices_clear_term_name.

func ClearTypeName

func ClearTypeName(tau TypeT) int32

ClearTypeName is the go version of yices_clear_type_name.

func CloseConfig

func CloseConfig(cfg *ConfigT)

CloseConfig is the go version of yices_free_config.

func CloseContext

func CloseContext(ctx *ContextT)

CloseContext is the go version of yices_free_context.

func CloseModel

func CloseModel(model *ModelT)

CloseModel is the go version of yices_free_model.

func CloseMpq

func CloseMpq(mpq *MpqT)

CloseMpq frees up a MpqT pointer.

func CloseMpz

func CloseMpz(mpz *MpzT)

CloseMpz frees MpzT pointer.

func CloseParamRecord

func CloseParamRecord(params *ParamT)

CloseParamRecord is the go version of yices_free_param_record.

func CompatibleTypes

func CompatibleTypes(tau TypeT, sigma TypeT) bool

CompatibleTypes is the go version of yices_compatible_types.

func ContextDisableOption

func ContextDisableOption(ctx ContextT, option string) int32

ContextDisableOption is the go version of yices_context_enable_option.

func ContextEnableOption

func ContextEnableOption(ctx ContextT, option string) int32

ContextEnableOption is the go version of yices_context_enable_option.

func DecrefTerm

func DecrefTerm(t TermT) int32

DecrefTerm is the go version of yices_decref_term.

func DecrefType

func DecrefType(tau TypeT) int32

DecrefType is the go version of yices_decref_type.

func DefaultConfigForLogic

func DefaultConfigForLogic(cfg ConfigT, logic string) int32

DefaultConfigForLogic is the go version of yices_default_config_for_logic.

func DefaultParamsForContext

func DefaultParamsForContext(ctx ContextT, params ParamT)

DefaultParamsForContext is the go version of yices_default_params_for_context.

func DeleteYvalVector

func DeleteYvalVector(v *YvalVectorT)

DeleteYvalVector is the go version of yices_delete_yval_vector.

func ErrorString

func ErrorString() string

ErrorString returns a copy of the value of yices_error_string().

func Exit

func Exit()

Exit cleans up the internal yices2 library data structures.

func ExportFormulaToDimacs

func ExportFormulaToDimacs(t TermT, filename string, simplify bool, status *SmtStatusT) (errcode int32)

ExportFormulaToDimacs is the go version of yices_export_formula_to_dimacs. Since 2.6.2

func ExportFormulasToDimacs

func ExportFormulasToDimacs(t []TermT, filename string, simplify bool, status *SmtStatusT) (errcode int32)

ExportFormulasToDimacs is the go version of yices_export_formulas_to_dimacs. Since 2.6.2

func FormulaTrueInModel

func FormulaTrueInModel(model ModelT, t TermT) int32

FormulaTrueInModel is the go version of yices_formula_true_in_model.

func FormulasTrueInModel

func FormulasTrueInModel(model ModelT, t []TermT) int32

FormulasTrueInModel is the go version of yices_formulas_true_in_model.

func GarbageCollect

func GarbageCollect(ts []TermT, taus []TypeT, keepNamed int32)

GarbageCollect is the go version of yices_garbage_collect.

func GetBoolValue

func GetBoolValue(model ModelT, t TermT, val *int32) int32

GetBoolValue is the go version of yices_get_bool_value.

func GetBvValue

func GetBvValue(model ModelT, t TermT, val []int32) int32

GetBvValue is the go version of yices_get_bv_value.

func GetDoubleValue

func GetDoubleValue(model ModelT, t TermT, val *float64) int32

GetDoubleValue is the go version of yices_get_double_value.

func GetInt32Value

func GetInt32Value(model ModelT, t TermT, val *int32) int32

GetInt32Value is the go version of yices_get_int32_value.

func GetInt64Value

func GetInt64Value(model ModelT, t TermT, val *int64) int32

GetInt64Value is the go version of yices_get_int64_value.

func GetMpqValue

func GetMpqValue(model ModelT, t TermT, val *MpqT) int32

GetMpqValue is the go version of yices_get_mpq_value.

func GetMpzValue

func GetMpzValue(model ModelT, t TermT, val *MpzT) int32

GetMpzValue is the go version of yices_get_mpz_value.

func GetRational32Value

func GetRational32Value(model ModelT, t TermT, num *int32, den *uint32) int32

GetRational32Value is the go version of yices_get_rational32_value.

func GetRational64Value

func GetRational64Value(model ModelT, t TermT, num *int64, den *uint64) int32

GetRational64Value is the go version of yices_get_rational64_value.

func GetScalarValue

func GetScalarValue(model ModelT, t TermT, val *int32) int32

GetScalarValue is the go version of yices_get_scalar_value.

func GetTermName

func GetTermName(t TermT) string

GetTermName is the go version of yices_get_term_name.

func GetTypeName

func GetTypeName(tau TypeT) string

GetTypeName is the go version of yices_get_type_name.

func GetValue

func GetValue(model ModelT, t TermT, val *YvalT) int32

GetValue is the go version of yices_get_value.

func HasDelegate

func HasDelegate(delegate string) bool

HasDelegate is the go version of yices_has_delegate. Since 2.6.2

func HasMcsat

func HasMcsat() int32

HasMcsat indicates if the yices2 library supports MCSAT.

func IncrefTerm

func IncrefTerm(t TermT) int32

IncrefTerm is the go version of yices_incref_term.

func IncrefType

func IncrefType(tau TypeT) int32

IncrefType is the go version of yices_incref_type.

func Init

func Init()

Init initializes the internal yices2 library data structures.

func InitConfig

func InitConfig(cfg *ConfigT)

InitConfig is the go version of yices_new_config.

func InitContext

func InitContext(cfg ConfigT, ctx *ContextT)

InitContext is the go version of yices_new_context.

func InitMpq

func InitMpq(mpq *MpqT)

InitMpq creates a MpqT.

func InitMpz

func InitMpz(mpz *MpzT)

InitMpz creates a MpzT.

func InitParamRecord

func InitParamRecord(params *ParamT)

InitParamRecord is the go version of yices_new_param_record.

func InitYvalVector

func InitYvalVector(v *YvalVectorT)

InitYvalVector is the go version of yices_init_yval_vector.

func IsThreadSafe

func IsThreadSafe() int32

IsThreadSafe indicate if the yices2 library was built with thread safety enabled. Since 2.6.2

func ModelToString

func ModelToString(model ModelT, width uint32, height uint32, offset uint32) string

ModelToString returns a pretty printed string representation of the given model.

func NumPosrefTerms

func NumPosrefTerms() uint32

NumPosrefTerms is the go version of yices_num_posref_terms.

func NumPosrefTypes

func NumPosrefTypes() uint32

NumPosrefTypes is the go version of yices_num_posref_types.

func NumTerms

func NumTerms() uint32

NumTerms is the go version of yices_num_terms.

func NumTypes

func NumTypes() uint32

NumTypes is the go version of yices_num_types.

func Pop

func Pop(ctx ContextT) int32

Pop is the go version of yices_pop.

func PpModel

func PpModel(file *os.File, model ModelT, width uint32, height uint32, offset uint32) int32

PpModel is the go version of yices_pp_model_fd(

func PpTerm

func PpTerm(file *os.File, t TermT, width uint32, height uint32, offset uint32) int32

PpTerm is the go version of yices_pp_term_fd

func PpTermArray

func PpTermArray(file *os.File, t []TermT, width uint32, height uint32, offset uint32, horiz int32) int32

PpTermArray is the go version of yices_pp_term_array_fd

func PpTermValues

func PpTermValues(file *os.File, model ModelT, t []TermT, width uint32, height uint32, offset uint32) int32

PpTermValues is the go version of yices_pp_term_values_fd Since 2.6.2

func PpType

func PpType(file *os.File, tau TypeT, width uint32, height uint32, offset uint32) int32

PpType is the go version of yices_pp_type_fd

func PrintError

func PrintError(f *os.File) int32

PrintError prints the most recent yices error out to the given file.

func PrintModel

func PrintModel(file *os.File, model ModelT) int32

PrintModel is the go version of yices_print_model_fd

func PrintTermValues

func PrintTermValues(file *os.File, model ModelT, t []TermT) int32

PrintTermValues is the go version of yices_print_term_values_fd Since 2.6.2

func ProductComponent

func ProductComponent(t TermT, i int32, term *TermT, exp *uint32) int32

ProductComponent is the go version of yices_product_component.

func ProjIndex

func ProjIndex(t TermT) int32

ProjIndex is the go version of yices_proj_index.

func Push

func Push(ctx ContextT) int32

Push is the go version of yices_push.

func RationalConstValue

func RationalConstValue(t TermT, q *MpqT) int32

RationalConstValue is the go version of yices_rational_const_value.

func RemoveTermName

func RemoveTermName(name string)

RemoveTermName is the go version of yices_remove_term_name.

func RemoveTypeName

func RemoveTypeName(name string)

RemoveTypeName is the go version of yices_remove_type_name.

func Reset

func Reset()

Reset resets up the internal yices2 library data structures.

func ResetContext

func ResetContext(ctx ContextT)

ResetContext is the go version of yices_reset_context.

func ResetYvalVector

func ResetYvalVector(v *YvalVectorT)

ResetYvalVector is the go version of yices_reset_yval_vector.

func ScalarConstValue

func ScalarConstValue(t TermT, val *int32) int32

ScalarConstValue is the go version of yices_scalar_const_value.

func ScalarTypeCard

func ScalarTypeCard(tau TypeT) uint32

ScalarTypeCard is the go version of yices_scalar_type_card.

func SetConfig

func SetConfig(cfg ConfigT, name string, value string) int32

SetConfig is the go version of yices_set_config.

func SetParam

func SetParam(params ParamT, pname string, value string) int32

SetParam is the go version of yices_set_param.

func SetTermName

func SetTermName(t TermT, name string) int32

SetTermName is the go version of yices_set_term_name.

func SetTypeName

func SetTypeName(tau TypeT, name string) int32

SetTypeName is the go version of yices_set_type_name.

func StopSearch

func StopSearch(ctx ContextT)

StopSearch is the go version of yices_stop_search.

func SumComponent

func SumComponent(t TermT, i int32, coeff *MpqT, term *TermT) int32

SumComponent is the go version of yices_sum_componentp.

func TermArrayValue

func TermArrayValue(model ModelT, a []TermT, b []TermT) int32

TermArrayValue is the go version of yices_term_array_value.

func TermBitsize

func TermBitsize(t TermT) uint32

TermBitsize is the go version of yices_term_bitsize.

func TermIsArithmetic

func TermIsArithmetic(t TermT) bool

TermIsArithmetic is the go version of yices_term_is_arithmetic.

func TermIsAtomic

func TermIsAtomic(t TermT) bool

TermIsAtomic is the go version of yices_term_is_atomic.

func TermIsBitvector

func TermIsBitvector(t TermT) bool

TermIsBitvector is the go version of yices_term_is_bitvector.

func TermIsBool

func TermIsBool(t TermT) bool

TermIsBool is the go version of yices_term_is_bool.

func TermIsBvsum

func TermIsBvsum(t TermT) bool

TermIsBvsum is the go version of yices_term_is_bvsum.

func TermIsComposite

func TermIsComposite(t TermT) bool

TermIsComposite is the go version of yices_term_is_composite.

func TermIsFunction

func TermIsFunction(t TermT) bool

TermIsFunction is the go version of yices_term_is_function.

func TermIsGround

func TermIsGround(t TermT) bool

TermIsGround is the go version of yices_term_is_ground.

func TermIsInt

func TermIsInt(t TermT) bool

TermIsInt is the go version of yices_term_is_int.

func TermIsProduct

func TermIsProduct(t TermT) bool

TermIsProduct is the go version of yices_term_is_product.

func TermIsProjection

func TermIsProjection(t TermT) bool

TermIsProjection is the go version of yices_term_is_projection.

func TermIsReal

func TermIsReal(t TermT) bool

TermIsReal is the go version of yices_term_is_real.

func TermIsScalar

func TermIsScalar(t TermT) bool

TermIsScalar is the go version of yices_term_is_scalar.

func TermIsSum

func TermIsSum(t TermT) bool

TermIsSum is the go version of yices_term_is_sum.

func TermIsTuple

func TermIsTuple(t TermT) bool

TermIsTuple is the go version of yices_term_is_tuple.

func TermNumChildren

func TermNumChildren(t TermT) int32

TermNumChildren is the go version of yices_term_num_children.

func TermToString

func TermToString(t TermT, width uint32, height uint32, offset uint32) string

TermToString returns a pretty printed string representation of the given term.

func TestSubtype

func TestSubtype(tau TypeT, sigma TypeT) bool

TestSubtype is the go version of yices_test_subtype.

func TypeIsArithmetic

func TypeIsArithmetic(tau TypeT) bool

TypeIsArithmetic is the go version of yices_type_is_arithmetic.

func TypeIsBitvector

func TypeIsBitvector(tau TypeT) bool

TypeIsBitvector is the go version of yices_type_is_bitvector.

func TypeIsBool

func TypeIsBool(tau TypeT) bool

TypeIsBool is the go version of yices_type_is_bool.

func TypeIsFunction

func TypeIsFunction(tau TypeT) bool

TypeIsFunction is the go version of yices_type_is_function.

func TypeIsInt

func TypeIsInt(tau TypeT) bool

TypeIsInt is the go version of yices_type_is_int.

func TypeIsReal

func TypeIsReal(tau TypeT) bool

TypeIsReal is the go version of yices_type_is_real.

func TypeIsScalar

func TypeIsScalar(tau TypeT) bool

TypeIsScalar is the go version of yices_type_is_scalar.

func TypeIsTuple

func TypeIsTuple(tau TypeT) bool

TypeIsTuple is the go version of yices_type_is_tuple.

func TypeIsUninterpreted

func TypeIsUninterpreted(tau TypeT) bool

TypeIsUninterpreted is the go version of yices_type_is_uninterpreted.

func TypeNumChildren

func TypeNumChildren(tau TypeT) int32

TypeNumChildren is the go version of yices_type_num_children.

func TypeToString

func TypeToString(tau TypeT, width uint32, height uint32, offset uint32) string

TypeToString returns a pretty printed string representation of the given type.

func ValBitsize

func ValBitsize(model ModelT, val *YvalT) uint32

ValBitsize is the go version of yices_val_bitsize.

func ValExpandTuple

func ValExpandTuple(model ModelT, yval *YvalT, child []YvalT) int32

ValExpandTuple is the go version of yices_val_expand_tuple.

func ValFunctionArity

func ValFunctionArity(model ModelT, val *YvalT) uint32

ValFunctionArity is the go version of yices_val_function_arity.

func ValGetBool

func ValGetBool(model ModelT, yval *YvalT, val *int32) int32

ValGetBool is the go version of yices_val_get_bool.

func ValGetBv

func ValGetBv(model ModelT, yval *YvalT, val []int32) int32

ValGetBv is the go version of yices_val_get_bv.

func ValGetDouble

func ValGetDouble(model ModelT, yval *YvalT, val *float64) int32

ValGetDouble is the go version of yices_val_get_double.

func ValGetInt32

func ValGetInt32(model ModelT, yval *YvalT, val *int32) int32

ValGetInt32 is the go version of yices_val_get_int32.

func ValGetInt64

func ValGetInt64(model ModelT, yval *YvalT, val *int64) int32

ValGetInt64 is the go version of yices_val_get_int64.

func ValGetMpq

func ValGetMpq(model ModelT, yval *YvalT, val *MpqT) int32

ValGetMpq is the go version of yices_val_get_mpq.

func ValGetMpz

func ValGetMpz(model ModelT, yval *YvalT, val *MpzT) int32

ValGetMpz is the go version of yices_val_get_mpz.

func ValGetRational32

func ValGetRational32(model ModelT, yval *YvalT, num *int32, den *uint32) int32

ValGetRational32 is the go version of yices_val_get_rational32.

func ValGetRational64

func ValGetRational64(model ModelT, yval *YvalT, num *int64, den *uint64) int32

ValGetRational64 is the go version of yices_val_get_rational64.

func ValGetScalar

func ValGetScalar(model ModelT, yval *YvalT, val *int32, tau *TypeT) int32

ValGetScalar is the go version of yices_val_get_scalar.

func ValIsInt32

func ValIsInt32(model ModelT, val *YvalT) int32

ValIsInt32 is the go version of yices_val_is_int32.

func ValIsInt64

func ValIsInt64(model ModelT, val *YvalT) int32

ValIsInt64 is the go version of yices_val_is_int64.

func ValIsInteger

func ValIsInteger(model ModelT, val *YvalT) int32

ValIsInteger is the go version of yices_val_is_integer.

func ValIsRational32

func ValIsRational32(model ModelT, val *YvalT) int32

ValIsRational32 is the go version of yices_val_is_rational32.

func ValIsRational64

func ValIsRational64(model ModelT, val *YvalT) int32

ValIsRational64 is the go version of yices_val_is_rational64.

func ValMappingArity

func ValMappingArity(model ModelT, val *YvalT) uint32

ValMappingArity is the go version of yices_val_mapping_arity.

func ValTupleArity

func ValTupleArity(model ModelT, val *YvalT) uint32

ValTupleArity is the go version of yices_val_tuple_arity.

func Version

func Version() string

Version is the yices2 library version.

Types

type ConfigT

type ConfigT struct {
	// contains filtered or unexported fields
}

ConfigT is a thin wrapper around a C pointer to a ctx_config_t struct. It is stored as a uintptr to avoid the scrutiny of the go GC.

type ContextT

type ContextT struct {
	// contains filtered or unexported fields
}

ContextT is a thin wrapper around a C pointer to a context_t struct. It is stored as a uintptr to avoid the scrutiny of the go GC.

type ErrorCodeT

type ErrorCodeT int32

ErrorCodeT is the analog of the error_code_t enum of the yices library.

const (
	NoError ErrorCodeT = iota
	ErrorInvalidType
	ErrorInvalidTerm
	ErrorInvalidConstantIndex
	ErrorInvalidVarIndex // Not used anymore
	ErrorInvalidTupleIndex
	ErrorInvalidRationalFormat
	ErrorInvalidFloatFormat
	ErrorInvalidBvbinFormat
	ErrorInvalidBvhexFormat
	ErrorInvalidBitshift
	ErrorInvalidBvextract
	ErrorInvalidBitextract // added 2014/02/17
	ErrorTooManyArguments
	ErrorTooManyVars
	ErrorMaxBvsizeExceeded
	ErrorDegreeOverflow
	ErrorDivisionByZero
	ErrorPosIntRequired
	ErrorNonnegIntRequired
	ErrorScalarOrUtypeRequired
	ErrorFunctionRequired
	ErrorTupleRequired
	ErrorVariableRequired
	ErrorArithtermRequired
	ErrorBitvectorRequired
	ErrorScalarTermRequired
	ErrorWrongNumberOfArguments
	ErrorTypeMismatch
	ErrorIncompatibleTypes
	ErrorDuplicateVariable
	ErrorIncompatibleBvsizes
	ErrorEmptyBitvector
	ErrorArithconstantRequired // added 2013/01/23
	ErrorInvalidMacro          // added 2013/03/31
	ErrorTooManyMacroParams    // added 2013/03/31
	ErrorTypeVarRequired       // added 2013/03/31
	ErrorDuplicateTypeVar      // added 2013/03/31
	ErrorBvtypeRequired        // added 2013/05/27
	ErrorBadTermDecref         // added 2013/10/03
	ErrorBadTypeDecref         // added 2013/10/03
	ErrorInvalidTypeOp         // added 2014/12/03
	ErrorInvalidTermOp         // added 2014/12/04
)

These are the go versions of the yices_types.h error_code (code <= 100 constants: Errors in type or term construction)

const (
	/*
	 * Parser errors
	 */
	ErrorInvalidToken ErrorCodeT = 100 + iota
	ErrorSyntaxError
	ErrorUndefinedTypeName
	ErrorUndefinedTermName
	ErrorRedefinedTypeName
	ErrorRedefinedTermName
	ErrorDuplicateNameInScalar
	ErrorDuplicateVarName
	ErrorIntegerOverflow
	ErrorIntegerRequired
	ErrorRationalRequired
	ErrorSymbolRequired
	ErrorTypeRequired
	ErrorNonConstantDivisor
	ErrorNegativeBvsize
	ErrorInvalidBvconstant
	ErrorTypeMismatchInDef
	ErrorArithError
	ErrorBvarithError
)

These are the go versions of the yices_types.h error_code (100 < code <= 300 constants: Parser errors)

const (
	/*
	 * These codes mean that the context as configured
	 * cannot process the assertions.
	 */
	ErrorCtxFreeVarInFormula ErrorCodeT = 300 + iota
	ErrorCtxLogicNotSupported
	ErrorCtxUfNotSupported
	ErrorCtxArithNotSupported
	ErrorCtxBvNotSupported
	ErrorCtxArraysNotSupported
	ErrorCtxQuantifiersNotSupported
	ErrorCtxLambdasNotSupported
	ErrorCtxNonlinearArithNotSupported
	ErrorCtxFormulaNotIdl
	ErrorCtxFormulaNotRdl
	ErrorCtxTooManyArithVars
	ErrorCtxTooManyArithAtoms
	ErrorCtxTooManyBvVars
	ErrorCtxTooManyBvAtoms
	ErrorCtxArithSolverException
	ErrorCtxBvSolverException
	ErrorCtxArraySolverException
	ErrorCtxScalarNotSupported // added 2015/03/26
	ErrorCtxTupleNotSupported  // added 2015/03/26
	ErrorCtxUtypeNotSupported  // added 2015/03/26
)

These are the go versions of the yices_types.h error_code (300 < code <= 400 constants: Errors in assertion processing.)

const (
	ErrorCtxInvalidConfig ErrorCodeT = 500 + iota
	ErrorCtxUnknownParameter
	ErrorCtxInvalidParameterValue
	ErrorCtxUnknownLogic
)

These are the go versions of the yices_types.h error_code (500 < code <= 600 constants: Errors in context configurations and search parameter settings.)

const (
	ErrorEvalUnknownTerm ErrorCodeT = 600 + iota
	ErrorEvalFreevarInTerm
	ErrorEvalQuantifier
	ErrorEvalLambda
	ErrorEvalOverflow
	ErrorEvalFailed
	ErrorEvalConversionFailed
	ErrorEvalNoImplicant
	ErrorEvalNotSupported
)

These are the go versions of the yices_types.h error_code (600 < code <= 700 constants: Error codes for model queries.)

const (
	ErrorMdlUnintRequired ErrorCodeT = 700 + iota
	ErrorMdlConstantRequired
	ErrorMdlDuplicateVar
	ErrorMdlFtypeNotAllowed
	ErrorMdlConstructionFailed
)

These are the go versions of the yices_types.h error_code (700 < code <= 800 constants: Error codes for model construction.)

const (
	ErrorYvalInvalidOp ErrorCodeT = 800 + iota
	ErrorYvalOverflow
	ErrorYvalNotSupported
)

These are the go versions of the yices_types.h error_code (800 < code <= 900 constants: Error codes in DAG/node queries.)

const (
	ErrorMdlGenTypeNotSupported ErrorCodeT = 900 + iota
	ErrorMdlGenNonlinear
	ErrorMdlGenFailed
)

These are the go versions of the yices_types.h error_code (900 < code <= 1000 constants: Error codes for model generalization.)

const (
	/*
	 * This is a symptom that a bug has been found.
	 */
	ErrorInternalException ErrorCodeT = 9999 + iota
)

These are the go versions of the yices_types.h error_code (9999< code constants: Catch-all code for anything else.)

const (
	ErrorMcsatErrorUnsupportedTheory ErrorCodeT = 1000 + iota
)

These are the go versions of the yices_types.h error_code (1000 < code <= 9000 constants: MCSAT error codes.)

const (
	ErrorOutputError ErrorCodeT = 9000 + iota
)

These are the go versions of the yices_types.h error_code (9000 < code <= 9999 constants: Input/output and system errors.)

func ErrorCode

func ErrorCode() ErrorCodeT

ErrorCode returns the most recent yices error code.

type GenModeT

type GenModeT int32

GenModeT is the go analog of the enum yices_gen_mode_t defined in yices_types.h.

const (
	GenDefault GenModeT = iota
	GenBySubst
	GenByProj
)

These are the go analogs of the elements of the enum yices_gen_mode_t defined in yices_types.h.

type ModelT

type ModelT struct {
	// contains filtered or unexported fields
}

ModelT is a thin wrapper around a C pointer to a model_t struct. It is stored as a uintptr to avoid the scrutiny of the go GC.

func GetModel

func GetModel(ctx ContextT, keepSubst int32) *ModelT

GetModel is the go version of yices_get_model.

func ModelFromMap

func ModelFromMap(vars []TermT, vals []TermT) *ModelT

ModelFromMap is the go version of yices_model_from_map.

type MpqT

type MpqT C.mpq_t

MpqT is defined so that we can refer to C.mpq_t outside of this package

type MpzT

type MpzT C.mpz_t

MpzT is defined so that we can refer to C.mpz_t outside of this package

type ParamT

type ParamT struct {
	// contains filtered or unexported fields
}

ParamT is a thin wrapper around a C pointer to a param_t struct. It is stored as a uintptr to avoid the scrutiny of the go GC.

type SmtStatusT

type SmtStatusT int32

SmtStatusT is the analog of smt_status_t defined in yices_types.h

const (
	StatusIdle SmtStatusT = iota
	StatusSearching
	StatusUnknown
	StatusSat
	StatusUnsat
	StatusInterrupted
	StatusError
)

These are the analogs to the elements of smt_status_t defined in yices_types.h

func CheckContext

func CheckContext(ctx ContextT, params ParamT) SmtStatusT

CheckContext is the go version of yices_check_context.

func CheckContextWithAssumptions

func CheckContextWithAssumptions(ctx ContextT, params ParamT, t []TermT) SmtStatusT

CheckContextWithAssumptions is the go version of yices_check_context_with_assumptions.

func CheckFormula

func CheckFormula(t TermT, logic string, delegate string, model *ModelT) (status SmtStatusT)

CheckFormula is the go version of yices_check_formula. Since 2.6.2

func CheckFormulas

func CheckFormulas(t []TermT, logic string, delegate string, model *ModelT) (status SmtStatusT)

CheckFormulas is the go version of yices_check_formulas. Since 2.6.2

func ContextStatus

func ContextStatus(ctx ContextT) SmtStatusT

ContextStatus is the go version of yices_context_status.

type TermConstructorT

type TermConstructorT int32

TermConstructorT is the analog of the enum term_constructor_t defined in yices_types.h

const (
	TrmCnstrConstructorError TermConstructorT = iota - 1 // to report an error

	// atomic terms
	TrmCnstrBoolConstant      TermConstructorT = iota // boolean constant
	TrmCnstrArithConstant                             // rational constant
	TrmCnstrBvConstant                                // bitvector constant
	TrmCnstrScalarConstant                            // constant of uninterpreted/scalar
	TrmCnstrVariable                                  // variable in quantifiers
	TrmCnstrUninterpretedTerm                         // (i.e. global variables can't be bound)

	// composite terms
	TrmCnstrIteTerm      // if-then-else
	TrmCnstrAppTerm      // application of an uninterpreted function
	TrmCnstrUpdateTerm   // function update
	TrmCnstrTupleTerm    // tuple constructor
	TrmCnstrEqTerm       // equality
	TrmCnstrDistinctTerm // distinct t_1 ... t_n
	TrmCnstrForallTerm   // quantifier
	TrmCnstrLambdaTerm   // lambda
	TrmCnstrNotTerm      // (not t)
	TrmCnstrOrTerm       // n-ary OR
	TrmCnstrXorTerm      // n-ary XOR

	TrmCnstrBvArray       // array of boolean terms
	TrmCnstrBvDiv         // unsigned division
	TrmCnstrBvRem         // unsigned remainder
	TrmCnstrBvSdiv        // signed division
	TrmCnstrBvSrem        // remainder in signed division (rounding to 0)
	TrmCnstrBvSmod        // remainder in signed division (rounding to -infinity)
	TrmCnstrBvShl         // shift left (padding with 0)
	TrmCnstrBvLshr        // logical shift right (padding with 0)
	TrmCnstrBvAshr        // arithmetic shift right (padding with sign bit)
	TrmCnstrBvGeAtom      // unsigned comparison: (t1 >= t2)
	TrmCnstrBvSgeAtom     // signed comparison (t1 >= t2)
	TrmCnstrArithGeAtom   // atom (t1 >= t2) for arithmetic terms: t2 is always 0
	TrmCnstrArithRootAtom // atom (0 <= k <= root_count(p)) && (x r root(p, k)) for r in <, <=, ==, !=, >, >=

	TrmCnstrAbs         // absolute value
	TrmCnstrCeil        // ceil
	TrmCnstrFloor       // floor
	TrmCnstrRdiv        // real division (as in x/y)
	TrmCnstrIdiv        // integer division
	TrmCnstrImod        // modulo
	TrmCnstrIsIntAtom   // integrality test: (is-int t)
	TrmCnstrDividesAtom // divisibility test: (divides t1 t2)

	// projections
	TrmCnstrSelectTerm // tuple projection
	BTrmCnstritTerm    // bit-select: extract the i-th bit of a bitvector

	// sums
	TrmCnstrBvSum    // sum of pairs a * t where a is a bitvector constant (and t is a bitvector term)
	ATrmCnstrrithSum // sum of pairs a * t where a is a rational (and t is an arithmetic term)

	// products
	TrmCnstrPowerProduct // power products: (t1^d1 * ... * t_n^d_n)

)

These are the elements of TermConstructorT, the analog of the enum elements of term_constructor_t defined in yices_types.h

func TermConstructor

func TermConstructor(t TermT) TermConstructorT

TermConstructor is the go version of yices_term_constructor.

type TermT

type TermT int32

TermT is the go analog on term_t defined in yices_types.h. Unclear if this is a wise move.

const NullTerm TermT = -1

NullTerm is the go analog of NULL_TERM defined in yices_types.h.

func Abs

func Abs(t1 TermT) TermT

Abs is the go version of yices_abs.

func Add

func Add(t1 TermT, t2 TermT) TermT

Add is the go version of yices_add.

func And

func And(conjuncts []TermT) TermT

And is the go version of yices_and.

func And2

func And2(arg1 TermT, arg2 TermT) TermT

And2 is the go version of yices_and2.

func And3

func And3(arg1 TermT, arg2 TermT, arg3 TermT) TermT

And3 is the go version of yices_and3.

func Application

func Application(fun TermT, argv []TermT) TermT

Application is the go version of yices_application.

func Application1

func Application1(fun TermT, arg1 TermT) TermT

Application1 is the unary go version of yices_application.

func Application2

func Application2(fun TermT, arg1 TermT, arg2 TermT) TermT

Application2 is the binary go version of yices_application.

func Application3

func Application3(fun TermT, arg1 TermT, arg2 TermT, arg3 TermT) TermT

Application3 is the ternary go version of yices_application.

func ArithEq0Atom

func ArithEq0Atom(t TermT) TermT

ArithEq0Atom is the go version of yices_arith_eq0_atom.

func ArithEqAtom

func ArithEqAtom(t1 TermT, t2 TermT) TermT

ArithEqAtom is the go version of yices_arith_eq_atom.

func ArithGeq0Atom

func ArithGeq0Atom(t TermT) TermT

ArithGeq0Atom is the go version of yices_arith_geq0_atom.

func ArithGeqAtom

func ArithGeqAtom(t1 TermT, t2 TermT) TermT

ArithGeqAtom is the go version of yices_arith_geq_atom.

func ArithGt0Atom

func ArithGt0Atom(t TermT) TermT

ArithGt0Atom is the go version of yices_arith_gt0_atom.

func ArithGtAtom

func ArithGtAtom(t1 TermT, t2 TermT) TermT

ArithGtAtom is the go version of yices_arith_gt_atom.

func ArithLeq0Atom

func ArithLeq0Atom(t TermT) TermT

ArithLeq0Atom is the go version of yices_arith_leq0_atom.

func ArithLeqAtom

func ArithLeqAtom(t1 TermT, t2 TermT) TermT

ArithLeqAtom is the go version of yices_arith_leq_atom.

func ArithLt0Atom

func ArithLt0Atom(t TermT) TermT

ArithLt0Atom is the go version of yices_arith_lt0_atom.

func ArithLtAtom

func ArithLtAtom(t1 TermT, t2 TermT) TermT

ArithLtAtom is the go version of yices_arith_lt_atom.

func ArithNeq0Atom

func ArithNeq0Atom(t TermT) TermT

ArithNeq0Atom is the go version of yices_arith_neq0_atom.

func ArithNeqAtom

func ArithNeqAtom(t1 TermT, t2 TermT) TermT

ArithNeqAtom is the go version of yices_arith_neq_atom.

func AshiftRight

func AshiftRight(t TermT, n uint32) TermT

AshiftRight is the go version of yices_ashift_right.

func Bitextract

func Bitextract(t TermT, n uint32) TermT

Bitextract is the go version of yices_bitextract.

func Bvadd

func Bvadd(t1 TermT, t2 TermT) TermT

Bvadd is the go version of yices_bvadd.

func Bvand

func Bvand(t []TermT) TermT

Bvand is the go version of yices_bvand.

func Bvand2

func Bvand2(t1 TermT, t2 TermT) TermT

Bvand2 is the go version of yices_bvand2.

func Bvand3

func Bvand3(t1 TermT, t2 TermT, t3 TermT) TermT

Bvand3 is the go version of yices_bvand3.

func Bvarray

func Bvarray(t []TermT) TermT

Bvarray is the go version of yices_bvarray.

func Bvashr

func Bvashr(t1 TermT, t2 TermT) TermT

Bvashr is the go version of yices_bvashr.

func Bvconcat

func Bvconcat(t []TermT) TermT

Bvconcat is the go version of yices_bvconcat.

func Bvconcat2

func Bvconcat2(t1 TermT, t2 TermT) TermT

Bvconcat2 is the go version of yices_bvconcat2.

func BvconstFromArray

func BvconstFromArray(a []int32) TermT

BvconstFromArray is the go version of yices_bvconst_from_array. iam: FIXME check that bits is restricted to len(a)

func BvconstInt32

func BvconstInt32(bits uint32, x int32) TermT

BvconstInt32 is the go version of yices_bvconst_int32.

func BvconstInt64

func BvconstInt64(bits uint32, x int64) TermT

BvconstInt64 is the go version of yices_bvconst_int64.

func BvconstMinusOne

func BvconstMinusOne(bits uint32) TermT

BvconstMinusOne is the go version of yices_bvconst_minus_one.

func BvconstMpz

func BvconstMpz(bits uint32, z MpzT) TermT

BvconstMpz is the go version of yices_bvconst_mpz.

func BvconstOne

func BvconstOne(bits uint32) TermT

BvconstOne is the go version of yices_bvconst_one.

func BvconstUint32

func BvconstUint32(bits uint32, x uint32) TermT

BvconstUint32 is the go version of yices_bvconst_uint32.

func BvconstUint64

func BvconstUint64(bits uint32, x uint64) TermT

BvconstUint64 is the go version of yices_bvconst_uint64.

func BvconstZero

func BvconstZero(bits uint32) TermT

BvconstZero is the go version of yices_bvconst_zero.

func Bvdiv

func Bvdiv(t1 TermT, t2 TermT) TermT

Bvdiv is the go version of yices_bvdiv.

func BveqAtom

func BveqAtom(t1 TermT, t2 TermT) TermT

BveqAtom is the go version of yices_bveq_atom.

func Bvextract

func Bvextract(t TermT, i uint32, j uint32) TermT

Bvextract is the go version of yices_bvextract.

func BvgeAtom

func BvgeAtom(t1 TermT, t2 TermT) TermT

BvgeAtom is the go version of yices_bvge_atom.

func BvgtAtom

func BvgtAtom(t1 TermT, t2 TermT) TermT

BvgtAtom is the go version of yices_bvgt_atom.

func BvleAtom

func BvleAtom(t1 TermT, t2 TermT) TermT

BvleAtom is the go version of yices_bvle_atom.

func Bvlshr

func Bvlshr(t1 TermT, t2 TermT) TermT

Bvlshr is the go version of yices_bvlshr.

func BvltAtom

func BvltAtom(t1 TermT, t2 TermT) TermT

BvltAtom is the go version of yices_bvlt_atom.

func Bvmul

func Bvmul(t1 TermT, t2 TermT) TermT

Bvmul is the go version of yices_bvmul.

func Bvnand

func Bvnand(t1 TermT, t2 TermT) TermT

Bvnand is the go version of yices_bvnand.

func Bvneg

func Bvneg(t TermT) TermT

Bvneg is the go version of yices_bvneg.

func BvneqAtom

func BvneqAtom(t1 TermT, t2 TermT) TermT

BvneqAtom is the go version of yices_bvneq_atom.

func Bvnor

func Bvnor(t1 TermT, t2 TermT) TermT

Bvnor is the go version of yices_bvnor.

func Bvnot

func Bvnot(t TermT) TermT

Bvnot is the go version of yices_bvnot.

func Bvor

func Bvor(t []TermT) TermT

Bvor is the go version of yices_bvor.

func Bvor2

func Bvor2(t1 TermT, t2 TermT) TermT

Bvor2 is the go version of yices_bvor2.

func Bvor3

func Bvor3(t1 TermT, t2 TermT, t3 TermT) TermT

Bvor3 is the go version of yices_bvor3.

func Bvpower

func Bvpower(t1 TermT, d uint32) TermT

Bvpower is the go version of yices_bvpower.

func Bvproduct

func Bvproduct(t []TermT) TermT

Bvproduct is the go version of yices_bvproduct.

func Bvrem

func Bvrem(t1 TermT, t2 TermT) TermT

Bvrem is the go version of yices_bvrem.

func Bvrepeat

func Bvrepeat(t TermT, n uint32) TermT

Bvrepeat is the go version of yices_bvrepeat.

func Bvsdiv

func Bvsdiv(t1 TermT, t2 TermT) TermT

Bvsdiv is the go version of yices_bvsdiv.

func BvsgeAtom

func BvsgeAtom(t1 TermT, t2 TermT) TermT

BvsgeAtom is the go version of yices_bvsge_atom.

func BvsgtAtom

func BvsgtAtom(t1 TermT, t2 TermT) TermT

BvsgtAtom is the go version of yices_bvsgt_atom.

func Bvshl

func Bvshl(t1 TermT, t2 TermT) TermT

Bvshl is the go version of yices_bvshl.

func BvsleAtom

func BvsleAtom(t1 TermT, t2 TermT) TermT

BvsleAtom is the go version of yices_bvsle_atom.

func BvsltAtom

func BvsltAtom(t1 TermT, t2 TermT) TermT

BvsltAtom is the go version of yices_bvslt_atom.

func Bvsmod

func Bvsmod(t1 TermT, t2 TermT) TermT

Bvsmod is the go version of yices_bvsmod.

func Bvsquare

func Bvsquare(t TermT) TermT

Bvsquare is the go version of yices_bvsquare.

func Bvsrem

func Bvsrem(t1 TermT, t2 TermT) TermT

Bvsrem is the go version of yices_bvsrem.

func Bvsub

func Bvsub(t1 TermT, t2 TermT) TermT

Bvsub is the go version of yices_bvsub.

func Bvsum

func Bvsum(t []TermT) TermT

Bvsum is the go version of yices_bvsum.

func Bvxnor

func Bvxnor(t1 TermT, t2 TermT) TermT

Bvxnor is the go version of yices_bvxnor.

func Bvxor

func Bvxor(t []TermT) TermT

Bvxor is the go version of yices_bvxor.

func Bvxor2

func Bvxor2(t1 TermT, t2 TermT) TermT

Bvxor2 is the go version of yices_bvxor2.

func Bvxor3

func Bvxor3(t1 TermT, t2 TermT, t3 TermT) TermT

Bvxor3 is the go version of yices_bvxor3.

func Ceil

func Ceil(t1 TermT) TermT

Ceil is the go version of yices_ceil.

func Constant

func Constant(tau TypeT, index int32) TermT

Constant is the go version of yices_constant.

func Distinct

func Distinct(argv []TermT) TermT

Distinct is the go version of yices_distinct.

func DividesAtom

func DividesAtom(t1 TermT, t2 TermT) TermT

DividesAtom is the go version of yices_divides_atom.

func Division

func Division(t1 TermT, t2 TermT) TermT

Division is the go version of yices_division.

func Eq

func Eq(lhs TermT, rhs TermT) TermT

Eq is the go version of yices_eq.

func Exists

func Exists(vars []TermT, body TermT) TermT

Exists is the go version of yices_exists.

func False

func False() TermT

False is the go version of yices_false.

func Floor

func Floor(t1 TermT) TermT

Floor is the go version of yices_floor.

func Forall

func Forall(vars []TermT, body TermT) TermT

Forall is the go version of yices_forall.

func GeneralizeModel

func GeneralizeModel(model ModelT, t TermT, elims []TermT, mode GenModeT) (formulas []TermT)

GeneralizeModel is the go version of yices_generalize_model.

func GeneralizeModelArray

func GeneralizeModelArray(model ModelT, a []TermT, elims []TermT, mode GenModeT) (formulas []TermT)

GeneralizeModelArray is the go version of yices_generalize_model_array.

func GetTermByName

func GetTermByName(name string) TermT

GetTermByName is the go version of yices_get_term_by_name.

func GetUnsatCore

func GetUnsatCore(ctx ContextT) (unsatCore []TermT)

GetUnsatCore is the go version of yices_get_unsat_core.

func GetValueAsTerm

func GetValueAsTerm(model ModelT, t TermT) TermT

GetValueAsTerm is the go version of yices_get_value_as_term.

func Idiv

func Idiv(t1 TermT, t2 TermT) TermT

Idiv is the go version of yices_idiv.

func Iff

func Iff(lhs TermT, rhs TermT) TermT

Iff is the go version of yices_iff.

func Imod

func Imod(t1 TermT, t2 TermT) TermT

Imod is the go version of yices_imod.

func ImplicantForFormula

func ImplicantForFormula(model ModelT, t TermT) (literals []TermT)

ImplicantForFormula is the go version of yices_implicant_for_formula.

func ImplicantForFormulas

func ImplicantForFormulas(model ModelT, t []TermT) (literals []TermT)

ImplicantForFormulas is the go version of yices_implicant_for_formulas.

func Implies

func Implies(lhs TermT, rhs TermT) TermT

Implies is the go version of yices_implies.

func Int32

func Int32(val int32) TermT

Int32 is the go version of yices_int32.

func Int64

func Int64(val int64) TermT

Int64 is the go version of yices_int64.

func IsIntAtom

func IsIntAtom(t TermT) TermT

IsIntAtom is the go version of yices_is_int_atom.

func Ite

func Ite(cond TermT, thenTerm TermT, elseTerm TermT) TermT

Ite is the go version of yices_ite.

func Lambda

func Lambda(vars []TermT, body TermT) TermT

Lambda is the go version of yices_lambda.

func ModelCollectDefinedTerms

func ModelCollectDefinedTerms(model ModelT) (terms []TermT)

ModelCollectDefinedTerms is the go version of yices_model_collect_defined_terms.

func ModelTermArraySupport

func ModelTermArraySupport(model ModelT, t []TermT) (support []TermT)

ModelTermArraySupport is the go version of yices_model_term_array_support.

func ModelTermSupport

func ModelTermSupport(model ModelT, t TermT) (support []TermT)

ModelTermSupport is the go version of yices_model_term_support.

func Mpq

func Mpq(q *MpqT) TermT

Mpq is the go version of yices_mpq.

func Mpz

func Mpz(z *MpzT) TermT

Mpz is the go version of yices_mpz.

func Mul

func Mul(t1 TermT, t2 TermT) TermT

Mul is the go version of yices_mul.

func Neg

func Neg(t1 TermT) TermT

Neg is the go version of yices_neg.

func Neq

func Neq(lhs TermT, rhs TermT) TermT

Neq is the go version of yices_neq.

func NewUninterpretedTerm

func NewUninterpretedTerm(tau TypeT) TermT

NewUninterpretedTerm is the go version of yices_new_uninterpreted_term.

func NewVariable

func NewVariable(tau TypeT) TermT

NewVariable is the go version of yices_new_variable.

func Not

func Not(arg TermT) TermT

Not is the go version of yices_not.

func Or

func Or(disjuncts []TermT) TermT

Or is the go version of yices_or.

func Or2

func Or2(arg1 TermT, arg2 TermT) TermT

Or2 is the go version of yices_or2.

func Or3

func Or3(arg1 TermT, arg2 TermT, arg3 TermT) TermT

Or3 is the go version of yices_or3.

func Pair

func Pair(arg1 TermT, arg2 TermT) TermT

Pair is the go version of yices_pair.

func ParseBvbin

func ParseBvbin(s string) TermT

ParseBvbin is the go version of yices_parse_bvbin.

func ParseBvhex

func ParseBvhex(s string) TermT

ParseBvhex is the go version of yices_parse_bvhex.

func ParseFloat

func ParseFloat(s string) TermT

ParseFloat is the go version of yices_parse_float.

func ParseRational

func ParseRational(s string) TermT

ParseRational is the go version of yices_parse_rational.

func ParseTerm

func ParseTerm(s string) TermT

ParseTerm is the go version of yices_parse_term.

func PolyInt32

func PolyInt32(a []int32, t []TermT) TermT

PolyInt32 is the go version of yices_poly_int32.

func PolyInt64

func PolyInt64(a []int64, t []TermT) TermT

PolyInt64 is the go version of yices_poly_int64.

func PolyMpq

func PolyMpq(q []MpqT, t []TermT) TermT

PolyMpq is the go version of yices_poly_mpq.

func PolyMpz

func PolyMpz(z []MpzT, t []TermT) TermT

PolyMpz is the go version of yices_poly_mpz.

func PolyRational32

func PolyRational32(num []int32, den []uint32, t []TermT) TermT

PolyRational32 is the go version of yices_poly_rational32.

func PolyRational64

func PolyRational64(num []int64, den []uint64, t []TermT) TermT

PolyRational64 is the go version of yices_poly_rational64.

func Power

func Power(t1 TermT, d uint32) TermT

Power is the go version of yices_power.

func Product

func Product(argv []TermT) TermT

Product is the go version of yices_product.

func ProjArg

func ProjArg(t TermT) TermT

ProjArg is the go version of yices_proj_arg.

func Rational32

func Rational32(num int32, den uint32) TermT

Rational32 is the go version of yices_rational32.

func Rational64

func Rational64(num int64, den uint64) TermT

Rational64 is the go version of yices_rational64.

func Redand

func Redand(t TermT) TermT

Redand is the go version of yices_redand.

func Redcomp

func Redcomp(t1 TermT, t2 TermT) TermT

Redcomp is the go version of yices_redcomp.

func Redor

func Redor(t TermT) TermT

Redor is the go version of yices_redor.

func RotateLeft

func RotateLeft(t TermT, n uint32) TermT

RotateLeft is the go version of yices_rotate_left.

func RotateRight

func RotateRight(t TermT, n uint32) TermT

RotateRight is the go version of yices_rotate_right.

func Select

func Select(index uint32, tuple TermT) TermT

Select is the go version of yices_select.

func ShiftLeft0

func ShiftLeft0(t TermT, n uint32) TermT

ShiftLeft0 is the go version of yices_shift_left0.

func ShiftLeft1

func ShiftLeft1(t TermT, n uint32) TermT

ShiftLeft1 is the go version of yices_shift_left1.

func ShiftRight0

func ShiftRight0(t TermT, n uint32) TermT

ShiftRight0 is the go version of yices_shift_right0.

func ShiftRight1

func ShiftRight1(t TermT, n uint32) TermT

ShiftRight1 is the go version of yices_shift_right1.

func SignExtend

func SignExtend(t TermT, n uint32) TermT

SignExtend is the go version of yices_sign_extend.

func Square

func Square(t1 TermT) TermT

Square is the go version of yices_square.

func Sub

func Sub(t1 TermT, t2 TermT) TermT

Sub is the go version of yices_sub.

func SubstTerm

func SubstTerm(vars []TermT, vals []TermT, t TermT) TermT

SubstTerm is the go version of yices_subst_term.

func SubstTermArray

func SubstTermArray(vars []TermT, vals []TermT, t []TermT) TermT

SubstTermArray is the go version of yices_subst_term_array.

func Sum

func Sum(argv []TermT) TermT

Sum is the go version of yices_sum.

func TermChild

func TermChild(t TermT, i int32) TermT

TermChild is the go version of yices_term_child.

func TermChildren

func TermChildren(t TermT) (children []TermT)

TermChildren is the go version of yices_term_children. Since 2.6.2

func Triple

func Triple(arg1 TermT, arg2 TermT, arg3 TermT) TermT

Triple is the go version of yices_triple.

func True

func True() TermT

True is the go version of yices_true.

func Tuple

func Tuple(argv []TermT) TermT

Tuple is the go version of yices_tuple.

func TupleUpdate

func TupleUpdate(tuple TermT, index uint32, value TermT) TermT

TupleUpdate is the go version of yices_tuple_update.

func Update

func Update(fun TermT, argv []TermT, value TermT) TermT

Update is the go version of yices_update.

func Update1

func Update1(fun TermT, arg1 TermT, value TermT) TermT

Update1 is the go version of yices_update1.

func Update2

func Update2(fun TermT, arg1 TermT, arg2 TermT, value TermT) TermT

Update2 is the go version of yices_update2.

func Update3

func Update3(fun TermT, arg1 TermT, arg2 TermT, arg3 TermT, value TermT) TermT

Update3 is the go version of yices_update3.

func Xor

func Xor(xorjuncts []TermT) TermT

Xor is the go version of yices_xor.

func Xor2

func Xor2(arg1 TermT, arg2 TermT) TermT

Xor2 is the go version of yices_xor2.

func Xor3

func Xor3(arg1 TermT, arg2 TermT, arg3 TermT) TermT

Xor3 is the go version of yices_xor3.

func Zero

func Zero() TermT

Zero is the go version of yices_zero.

func ZeroExtend

func ZeroExtend(t TermT, n uint32) TermT

ZeroExtend is the go version of yices_zero_extend.

type TypeT

type TypeT int32

TypeT is the analog of term_t defined in yices_types.h. Unclear if this is a good idea.

const NullType TypeT = -1

NullType is the go version of NULL_TYPE.

func BoolType

func BoolType() TypeT

BoolType is the go version of yices_bool_type.

func BvType

func BvType(size uint32) TypeT

BvType is the go version of yices_bv_type.

func FunctionType

func FunctionType(dom []TypeT, rng TypeT) TypeT

FunctionType is the go version of yices_function_type.

func FunctionType1

func FunctionType1(tau1 TypeT, rng TypeT) TypeT

FunctionType1 is the unary go version of yices_function_type.

func FunctionType2

func FunctionType2(tau1 TypeT, tau2 TypeT, rng TypeT) TypeT

FunctionType2 is the binary go version of yices_function_type.

func FunctionType3

func FunctionType3(tau1 TypeT, tau2 TypeT, tau3 TypeT, rng TypeT) TypeT

FunctionType3 is the ternaery go version of yices_function_type.

func GetTypeByName

func GetTypeByName(name string) TypeT

GetTypeByName is the go version of yices_get_type_by_name.

func IntType

func IntType() TypeT

IntType is the go version of yices_int_type.

func NewScalarType

func NewScalarType(card uint32) TypeT

NewScalarType is the go version of yices_new_scalar_type.

func NewUninterpretedType

func NewUninterpretedType() TypeT

NewUninterpretedType is the go version of yices_new_uninterpreted_type.

func ParseType

func ParseType(s string) TypeT

ParseType is the go version of yices_parse_type.

func RealType

func RealType() TypeT

RealType is the go version of yices_real_type.

func TupleType

func TupleType(tau []TypeT) TypeT

TupleType is the go version of yices_tuple_type.

func TupleType1

func TupleType1(tau1 TypeT) TypeT

TupleType1 is the unary go version of yices_tuple_type.

func TupleType2

func TupleType2(tau1 TypeT, tau2 TypeT) TypeT

TupleType2 is the binary go version of yices_tuple_type.

func TupleType3

func TupleType3(tau1 TypeT, tau2 TypeT, tau3 TypeT) TypeT

TupleType3 is the ternary go version of yices_tuple_type.

func TypeChild

func TypeChild(tau TypeT, i int32) TypeT

TypeChild is the go version of yices_type_child.

func TypeChildren

func TypeChildren(tau TypeT) (children []TypeT)

TypeChildren is the go version of yices_type_children.

func TypeOfTerm

func TypeOfTerm(t TermT) TypeT

TypeOfTerm is the go version of yices_type_of_term.

func ValFunctionType

func ValFunctionType(model ModelT, val *YvalT) TypeT

ValFunctionType is the go version of yices_val_function_type. Since 2.6.2

type YicesErrorT

type YicesErrorT struct {
	ErrorString string
	Code        ErrorCodeT
	Line        uint32
	Column      uint32
	Term1       TermT
	Type1       TypeT
	Term2       TermT
	Type2       TypeT
	Badval      int64
}

YicesErrorT is the go representation of the yices_error_t struct of yices library.

func YicesError

func YicesError() (yerror *YicesErrorT)

YicesError returns a copy of the current error state

func (*YicesErrorT) Error

func (yerror *YicesErrorT) Error() string

Error returns the error's current error string.

func (*YicesErrorT) String

func (yerror *YicesErrorT) String() string

String returns the error string component of the YicesErrorT struct.

type YvalT

type YvalT C.yval_t

YvalT is the go analog of yval_t defined in yices_types.h

func ValExpandFunction

func ValExpandFunction(model ModelT, yval *YvalT, def *YvalT) (vector []YvalT)

ValExpandFunction is the go version of yices_val_expand_function.

func ValExpandMapping

func ValExpandMapping(model ModelT, m *YvalT, val *YvalT) (vector []YvalT)

ValExpandMapping is the go version of yices_val_mapping_arity.

type YvalTagT

type YvalTagT int32

YvalTagT is the go version of the yval_tag_t enum

const (
	YvalUnknown YvalTagT = iota
	YvalBool
	YvalRational
	YvalAlgebraic
	YvalBv
	YvalScalar
	YvalTuple
	YvalFunction
	YvalMapping
)

The corresponding element of the YvalTagT enum

func GetTag

func GetTag(yval YvalT) YvalTagT

GetTag accesses the node_tag of a YvalT object.

type YvalVectorT

type YvalVectorT C.yval_vector_t

YvalVectorT is the go analog of yval_vector_t defined in yices_types.h

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
t or T : Toggle theme light dark auto
y or Y : Canonical URL