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

Source Files

View all

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.