forked from aclements/go-z3
/
package.go
70 lines (65 loc) · 2.92 KB
/
package.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
// Copyright 2017 The Go Authors. All rights reserved.
// Use of this source code is governed by a BSD-style
// license that can be found in the LICENSE file.
// Package z3 checks the satisfiability of logical formulas.
//
// This package provides bindings for the Z3 SMT solver
// (https://github.com/Z3Prover/z3). Z3 checks satisfiability of
// logical formulas over a wide range of terms, including booleans,
// integers, reals, bit-vectors, and uninterpreted functions. For a
// good introduction to the concepts of SMT and Z3, see the Z3 guide
// (http://rise4fun.com/z3/tutorialcontent/guide).
//
// This package does not yet support all of the features or types
// supported by Z3, though it supports a reasonably large subset.
//
// The main entry point to the z3 package is type Context. All values
// are created and all solving is done relative to some Context, and
// values from different Contexts cannot be mixed.
//
// Symbolic values implement the Value interface. Every value has a
// type, called a "sort" and represented by type Sort. Sorts fall into
// general categories called "kinds", such as Bool and Int. Each kind
// corresponds to a different concrete type that implements the Value
// interface, since the kind determines the set of operations that
// make sense on a value. A Bool expression is also called a
// "formula".
//
// These concrete value types help with type checking expressions, but
// type checking is ultimately done dynamically by Z3. Attempting to
// create a badly typed value will panic.
//
// Symbolic values are represented as expressions of numerals,
// constants, and uninterpreted functions. A numeral is a literal,
// fixed value like "2". A constant is a term like "x", whose value is
// fixed but unspecified. An uninterpreted function is a function
// whose mapping from arguments to results is fixed but unspecified
// (this is in contrast to an "interpreted function" like + whose
// interpretation is specified to be addition). Functions are pure
// (side-effect-free) like mathematical functions, but unlike
// mathematical functions they are always total. A constant can be
// thought of as a function with zero arguments.
//
// It's possible to go back and forth between a symbolic value and the
// expression representing that value using Value.AsAST and
// AST.AsValue.
//
// Type Solver checks the satisfiability of a set of formulas. If the
// Solver determines that a set of formulas is satisfiable, it can
// construct a Model giving a specific assignment of constants and
// uninterpreted functions that satisfies the set of formulas.
package z3
/*
#include <stdbool.h>
*/
import "C"
// As of z3 4.7.1, Z3_bool is just an alias for C bool (prior to this
// it was an int, which is really why we have these functions). Z3
// 4.11 drops Z3_bool entirely, so for maximum forwards-compatibility,
// we use C bool.
func boolToZ3(b bool) C.bool {
return C.bool(b)
}
func z3ToBool(b C.bool) bool {
return bool(b)
}