solve

package
v0.2.0 Latest Latest
Warning

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

 Go to latest Published: Aug 24, 2026 License: Apache-2.0 Imports: 21 Imported by: 0

Documentation

Overview

Package solve translates the conditions a constraint, requirement or satisfaction assertion states into a solver-independent term IR and writes that IR as an SMT-LIB2 script.

It also runs an external solver over that script — z3 or cvc5, found on PATH or named by OPENSYSML_SMT — as a process speaking SMT-LIB2 on standard input, so no library is linked in and releases stay pure Go. The verdicts sat, unsat and unknown stay distinct: a timeout or arithmetic the solver gave up on is unknown, and a solver that crashes, is absent, or replies unusably is a typed error rather than a verdict.

The runtime evaluator remains the normative semantics; SysML v2 defines no solving semantics, so this is an advertised extension, not a conformance claim.

Solver compatibility

OPENSYSML_SMT names any executable that speaks SMT-LIB2 on standard input, so what a backend must support is stated rather than assumed of z3.

Logic selection emits the narrowest logic of the SMT-LIB 2.6 logic list (https://smt-lib.org/logics.shtml) that covers what a query actually uses: QF_UF for constants alone, QF_LIA/QF_NIA over Int, QF_LRA/QF_NRA over Real, and AUFLIRA/AUFNIRA for a query over both, the list defining no quantifier-free mixed logic to narrow to. Truncating integer division by a literal divisor stays in the linear logic — `div` and `mod` are the Ints theory's, which those logics include — and a variable divisor selects the nonlinear one it really needs. Datatypes and strings have no logic in the list, so a query using either sets the non-standard NonStandardLogic ("ALL"), which both verified backends accept; the script says so in a comment, and LogicChoice.Standard reports it. No logic is widened to dodge a hard case.

What a backend is required to support is a Capability, and a Solver is probed once per executable (cached, one small script per form of the feature the writer emits — QF_NIA and QF_NRA for nonlinear, AUFLIRA and AUFNIRA for mixed — and only for the capabilities a query and operation actually need) or declared capable by the caller (Solver.Declared). A capability the backend rejects — an `(error …)` reply or `unsupported` — makes the request an UnsupportedCapabilityError naming the backend, the feature and the operation, refused before any query is run: no silent degrade and no fabricated verdict. A check the backend neither answered nor rejected settles nothing, so the query proceeds and its own verdict or SolverProcessError is reported.

Three answers to a check are told apart, so a backend is never blamed for the wrong thing:

  • `(error …)`, `unsupported`, or a defined reply that contradicts the check — the backend refuses the capability, reported as UnsupportedCapabilityError.
  • `unknown`, no reply, a closed pipe or the check's deadline — nothing was established, so the query runs and answers for itself.
  • a reply SMT-LIB does not define at all, such as `maybe` — the executable is not answering as a solver, reported as SolverProcessError rather than as a missing feature, which is also how the dialogue itself reports one.

Probed against z3 4.8.12 and cvc5 1.3.4: both support models, unsat cores, incremental checks, datatypes, strings, div/mod, nonlinear and mixed arithmetic and the non-standard logic. cvc5 rejects `(maximize …)` as a parse error and answers `unsupported` to `:opt.priority`, both z3 extensions, so objective optimization is z3-only. internal/core/solve's portability harness (portability_test.go, TestPortability) runs one query per feature against whatever OPENSYSML_SMT names and reports each as pass, refuse or fail, a rejected script being ours to fix in the writer.

Conflict explanation

Explain answers an unsat verdict with the assertions that conflict. The script it writes (CoreScript) names each assertion, turns unsat cores on and asks for the core once the verdict is unsat; labels are the assertion's position, so a core reads back to the Assertion, and its Provenance, that produced it. Every role can appear in a core, a declared domain (RoleDomain) or a well-definedness guard (RoleDefined) included, and an inherited condition names the supertype that declared it.

Minimality is established, not assumed. A solver's core is unsatisfiable but need not be irreducible, so reduction drops one member at a time, each round a fresh solver process, and Core.Minimal says every remaining member was shown to be needed: dropping any one left the rest satisfiable. Reduction is bounded, in the spirit of the runtime's step budgets, by DefaultMaxCoreMembers members and DefaultCoreBudget of wall time (OPENSYSML_SMT_CORE_BUDGET overrides it); a core too large, out of budget, or whose round the solver did not decide is reported as it stands with Minimal false and Core.Note saying why. A solver that refuses cores, names an assertion the query did not assert, answers unreadably or reports an empty core is a CoreError, never an empty or invented core.

Conditions come from the evaluator's own collection (runtime.Context.ConditionsOf), keeping its order and its distinctions: `require` versus `assume`, negation, and a body meaning the conjunction of its conditions.

Differential agreement gate

The translation is evidence-backed rather than asserted: for an element whose conditions translate, and for a concrete assignment of the features they read, the gate (differential_test.go and the corpus and randomized gates beside it) requires the query conjoined with that assignment to be sat exactly when the evaluator says the conditions hold, and unsat exactly when it says they do not. Every other outcome is classified, never averaged away: unknown is recorded, a typed evaluator error is no verdict, and ErrDivisionByZero is required to correspond to the guarded query being unsat for that assignment.

It runs over the runtime conformance corpus, the bundled standard library, the OMG training corpus and deterministic randomized models, and reports how much of each it reached — translated, refused, agreed, disagreed, unknown — so coverage drift is reviewable. What it proves is that the translation is faithful to the evaluator on the cases it covered; it is not a conformance claim, and the evaluator remains normative where the two ever differ.

Translatable subset

A condition is translatable when every part of it is:

  • Boolean operators: `not`, `and`, `&`, `or`, `|`, `xor`, `implies`, and the conditional expression `if c ? a else b`.
  • Equality `==` and `!=` between two values of the same sort.
  • Comparisons `<`, `<=`, `>`, `>=` between numbers of the same dimension.
  • Arithmetic `+`, `-`, `*`, unary `-` and `+`.
  • Division `/` and remainder `%`. Integer division truncates toward zero as the evaluator does, encoded as ite(a >= 0, div(a, b), -div(-a, b)), and the remainder as a - b*tdiv(a, b), which takes the dividend's sign. A literal divisor keeps this linear; a variable divisor sets Query.Nonlinear, so unknown is an expected verdict rather than a surprise.
  • Division by zero, which SMT-LIB leaves underspecified while the evaluator refuses it: a literal zero divisor refuses translation, and any other divisor, integer or real, is asserted non-zero as a RoleDefined side condition. That assertion constrains the whole query, so it is only made where the division is always evaluated and read unnegated; a computed divisor under `not`, `or`, `xor`, `implies`, a conditional branch or a denied element refuses instead, since the evaluator may never divide there.
  • Literals: boolean, integer, real, string.
  • Quantity expressions (`450.0 [km/h]`), normalized to the base units their unit reduces to through semantics.UnitTermOf — magnitudes are exact rationals, so a scale factor introduces no rounding.
  • References to scalar-valued features, resolved through the same names the evaluator resolves: Boolean, String, Natural (declared non-negative), Integer, Rational, Real and Number features, features typed by a quantity value type, enumeration-typed features and variation points.
  • Feature chains that ground in such a feature (`lander.verticalSpeed`).
  • Enumeration literals and variants, as constructors of a finite datatype sort declared per enumeration definition or variation point.

A variable stands for the value a feature may take, constrained only by its sort: declared values are not asserted, so a query asks what the conditions permit rather than what one object holds.

Value synthesis

TranslateWith (and ConstraintWith, RequirementWith, SatisfactionWith) takes a partial assignment: Pins fixing some features to the values the model already fixes, the rest left free for the solver to choose. A pin is read where the evaluator reads it — Fixed and FixedFor go through the runtime's objects, feature values and declared defaults — and carries its provenance: held by an object (PinHeld), declared by the model (PinDeclared) or chosen by the caller (PinChosen). Passing no pin translates exactly as before, so a query with no partial assignment is the same script it always was.

A pin becomes an ordinary equality assertion in role RolePinned, asserted before the conditions and named in Query.Pinned with its assertion index, so it can appear in an unsat core like any other assertion: unsat under pins means no values exist consistent with what is already fixed, and the core says which fixed values conflict. Values are converted through the same machinery the translator uses — a quantity normalized to base units as an exact rational, an enumeration literal or variant as the datatype constructor the writer declares — and a value the subset cannot represent, or one whose dimension does not match its feature, is a PinError wrapping ErrNotPinnable, never a silent drop. Features read by the conditions but not readable as a value are reported as Unread rather than being fixed to something.

Result.Model is one witness, not a canonical answer: a satisfiable query usually has many models and the solver may return any of them. Values are rendered in OpenSysML's terms where the sort allows (qualified feature names, declared units, enumeration and variant names) and flagged as the solver wrote them where it does not.

Variant configuration

A variation point translates as a finite datatype sort (Sort.Variation), so Query.Variations are its variation variables. Query.FixValue chooses a variant (PinChosen), which Solve then checks like any other fixed value, and with none chosen Solve's model is a consistent selection. Configurations enumerates consistent selections: one fresh check-sat per solution, each asserting the negation of the complete previous assignment, built from the solver's own terms rather than from rendered text. Every variation variable is assigned in every solution, nested variation points and constrained variants included, since they are variables of the same query as any other condition.

The enumeration is bounded, in the spirit of the runtime's step budgets, by DefaultMaxConfigurations solutions (OPENSYSML_SMT_MAX_CONFIGURATIONS overrides it). Result.Truncated says the enumeration was cut short and why: AtBound for the bound, Undecided for a solver that stopped deciding, with TimedOut when the run's deadline was what stopped it — a deadline reports the solutions already found rather than discarding them. Results are exhaustive only when a final check-sat answered unsat; nothing implies exhaustiveness that was not shown. A query reading no variation point is a NoVariationsError wrapping ErrNoVariations, not an empty enumeration.

Known limitations: only variation points in the translatable subset are configured, so a variation whose variants carry collection-valued or otherwise untranslatable conditions refuses with ErrNotTranslatable; variants are configured as values of a variation point, not as objects, so nothing is materialized and features a variant would only have once bound are not constrained; and the enumeration order is the solver's, not a defined one.

Objective optimization

Analysis and AnalysisWith translate an `analysis def` as an optimization query: what its conditions permit, and the objectives to improve within that. Solver.Optimize then asks a backend for each objective's optimum.

SysML v2 states no direction, value or solving semantics for `objective`, so this layer states the contract it reads (an OpenSysML extension, not a conformance claim):

  • Direction comes from the trade-study definition the objective is typed by: TradeStudies::MinimizeObjective or MaximizeObjective, specializations included. An objective typed by neither refuses with ErrNotOptimizable.
  • The value to improve is the expression the objective states for the library's `best` feature — `objective o : MinimizeObjective { attribute :>> best = expression; }` — since an objective is a requirement usage and carries no scalar value of its own. A value bound directly to the objective is read too, where a model can write one.
  • What is feasible is the case's own conditions (CaseConditionsOf: `require`, `assume`, `assert`, `inv`, inherited ones included) together with the conditions each objective states: its own body's, and the ones it inherits from the model's own objective definitions, read where they are inherited. Only the trade-study library's own conditions are left out, being about choosing among alternatives rather than about which values are feasible. A condition an inherited definition states over `best` bounds the value improved, since the objective's `best` is asserted equal to it (RoleDefined). A case stating no condition is legitimately unbounded, not refused.
  • Objectives, values and conditions are read through the runtime's own surfaces (runtime.Context.ObjectivesOf), so what is optimized is what the evaluator would evaluate; no declaration is re-parsed and no AST mutated.

The objective term must be numeric and linear: an optimizer improves a linear objective, so a product or quotient of two computed values refuses with ErrNotOptimizable rather than being sent and misread. Divisor guards therefore sit in the conditions, where a computed divisor is asserted non-zero as usual.

Multiple objectives, and backend requirements

Several objectives are optimized lexicographically in declaration order: each within what the ones before it already settled. The script says so itself with `(set-option :opt.priority lex)` rather than relying on a backend default — z3's `box` mode reports each objective's optimum separately and returns a model attaining only one of them, which would make "the assignments achieving the optimum" untrue.

`(minimize e)`/`(maximize e)`, `(get-objectives)` and `:opt.priority` are solver extensions rather than SMT-LIB2; cvc5 implements none of them. Solver.Optimize settles them through the capability model below before sending a query — CapOptimization and CapOptimizationPriority, probed once per backend and cached — and reports a backend without them as NoOptimizationError, which wraps both ErrNoOptimization and the ErrUnsupportedCapability refusal it was settled by. Nothing is ever degraded to a plain check-sat and presented as an optimum.

What an optimum is, and is not

Optimum.Status keeps the cases apart, and no case fabricates a number:

  • OptimumAttained: the value reported is the optimum and an assignment attains it. Both are checked here rather than taken on the backend's word: the objective's value in the reported model is read back, and a further check asks whether any assignment does lexicographically better — better in an earlier objective, or equal there and better in a later one. Unsat is what makes the answer an optimum.
  • OptimumUnbounded: the conditions permit arbitrarily better values (`oo`).
  • OptimumBounded: the objective approaches a bound no assignment attains, as a strict inequality over the reals does. Backends report this as an infinitesimal (`(+ 10.5 (* (- 1.0) epsilon))`) or an interval; the bound is reported as a bound, never as an attained value.
  • OptimumUnverified: the backend reported a value a better feasible value refutes. z3 4.8.12 does this for open real suprema — maximizing x under x < 10.5 reports 9.5 — which is why every optimum is verified rather than trusted.
  • OptimumUndecided: verification did not decide, or the answer was no number.

Optimum.Feasible is always a value the reported assignment attains: a witness the conditions permit, not an optimum. A solver answering sat but refusing to report its objectives readably is an OptimumError wrapping ErrNoOptimum and ErrSolverProcess; unsat and unknown stay the verdicts they are, with no optima invented for them, and a query stating no objective is a NoObjectiveError wrapping ErrNoObjective rather than a satisfiability check.

Deliberately out of subset

Everything else refuses with ErrNotTranslatable, and one refused conjunct fails the whole query, so no partial script exists:

  • Collections and quantifiers: sequences, sets, `->select`, `->collect`, `->forAll`, `->exists`, `->size`, indexing `#(i)`, ranges `a..b`, and collection-valued features. Bounded expansion is not implemented.
  • Invocations of any kind, calc usages included: a calc body may be iterative or read state, and constant folding it is the evaluator's job.
  • Euclidean `div`/`mod` themselves, as SMT-LIB defines them: only the evaluator's truncating semantics are encoded.
  • Real remainder `%`, which the evaluator answers by floating-point remainder.
  • `**` and `^`: exponentiation is outside linear and polynomial arithmetic as encoded here.
  • Classification and metadata operators: `hastype`, `istype`, `@`, `@@`, `as`, `meta`, `all`, `===`, `!==`, `??`, `~`, and `null`.
  • Complex numbers, string operations other than equality, and features whose type determines no scalar sort.
  • Comparing or adding magnitudes of different dimensions, which the evaluator reports as incommensurable units.
  • Unresolved names and feature chains that ground in nothing.

Index

Constants

View Source 
const CoreBudgetEnv = "OPENSYSML_SMT_CORE_BUDGET"

CoreBudgetEnv names the environment variable that overrides how long a core may be shrunk for, as a Go duration ("5s", "500ms").

View Source 
const DefaultCoreBudget = 30 * time.Second

DefaultCoreBudget is how long reduction is given in total, in the spirit of the runtime's step budgets: past it the solver's own core is reported as it came, said to be not necessarily minimal.

View Source 
const DefaultMaxConfigurations = 32

DefaultMaxConfigurations bounds how many configurations one enumeration reports. The combinations grow as the product of the variants of every variation point read, so the bound is what stops a runaway enumeration; results stopped by it are reported as truncated rather than as all there are.

View Source 
const DefaultMaxCoreMembers = 64

DefaultMaxCoreMembers is the largest core reduction is attempted over, since each dropped candidate costs a solver call.

View Source 
const DefaultTimeout = 10 * time.Second

DefaultTimeout is how long a solver is given to answer one query before the verdict becomes `unknown`, in the spirit of the runtime's step budgets.

View Source 
const MaxConfigurationsEnv = "OPENSYSML_SMT_MAX_CONFIGURATIONS"

MaxConfigurationsEnv names the environment variable that overrides how many configurations one enumeration reports.

View Source 
const NonStandardLogic = "ALL"

NonStandardLogic is the logic a script sets when no SMT-LIB logic covers what it uses. The SMT-LIB 2.6 logic list names no logic with algebraic datatypes or with strings, so a query using either sets this, which z3 and cvc5 accept.

View Source 
const ProbeTimeout = 10 * time.Second

ProbeTimeout is how long one capability check is given. The checks are tiny, so a backend that does not answer in this long is refusing rather than working.

View Source 
const SolverEnv = "OPENSYSML_SMT"

SolverEnv names the environment variable that overrides solver discovery with the path of an executable speaking SMT-LIB2 on standard input.

View Source 
const TimeoutEnv = "OPENSYSML_SMT_TIMEOUT"

TimeoutEnv names the environment variable that overrides how long a solver is given, as a Go duration ("5s", "500ms").

Variables

View Source 
var (
	Bool   = Sort{Kind: SortBool, Name: "Bool"}
	Int    = Sort{Kind: SortInt, Name: "Int"}
	Real   = Sort{Kind: SortReal, Name: "Real"}
	String = Sort{Kind: SortString, Name: "String"}
)

The scalar sorts, which every query may use without declaring them.

View Source 
var AllCapabilities = []Capability{
	CapModels, CapUnsatCores, CapIncremental, CapDatatypes, CapStrings,
	CapIntegerDivision, CapNonlinearArith, CapMixedArith, CapNonStandardLogic,
	CapOptimization, CapOptimizationPriority,
}

AllCapabilities are every capability, in declaration order: what a probe reports on and what a compatibility table lists.

View Source 
var ErrNoConditions = errors.New("states no condition")

ErrNoConditions is returned for an element that states no condition to translate, as evaluating it reports the same.

View Source 
var ErrNoCore = errors.New("the SMT solver did not report an unsat core")

ErrNoCore is returned when a solver answered unsat but would not report which assertions conflict, or named assertions the query never asserted. No core is invented in its place.

View Source 
var ErrNoObjective = errors.New("states no objective")

ErrNoObjective is returned for an analysis case that states no objective, so there is nothing to optimize: what it permits is still a satisfiability question, which checking it plainly answers.

View Source 
var ErrNoOptimization = errors.New("the SMT solver does not implement optimization")

ErrNoOptimization is returned when the solver found does not implement optimization. `(maximize …)` is a z3 extension rather than SMT-LIB, so this is reported rather than degraded to a plain satisfiability check.

View Source 
var ErrNoOptimum = errors.New("the SMT solver did not report the optimum")

ErrNoOptimum is returned when a solver answered sat but did not report the optimum readably. No optimum is invented in its place.

View Source 
var ErrNoSolver = errors.New("no SMT solver found")

ErrNoSolver is returned when no SMT solver could be found to run a query. Solving is optional, so its absence is reported rather than passed over.

View Source 
var ErrNoVariations = errors.New("no variation point is read")

ErrNoVariations is returned for a query whose conditions read no variation point, so there is no configuration to check or enumerate: the element may still be satisfiable, which is what solving it plainly answers.

View Source 
var ErrNotOptimizable = errors.New("not optimizable")

ErrNotOptimizable is returned for an objective that cannot be optimized as written: it states no direction, no value, or a value an optimizer cannot improve. It is a refusal about the objective rather than about the subset a condition is translated in.

View Source 
var ErrNotPinnable = errors.New("value cannot be fixed for solving")

ErrNotPinnable is returned for a value that cannot be fixed in a query: one the term language has no literal for, or one whose type or dimension does not match the variable it would fix. A pin is never dropped silently, since a query missing one would answer about values the model does not hold.

View Source 
var ErrNotTranslatable = errors.New("not translatable for solving")

ErrNotTranslatable is returned when a condition uses a construct outside the translatable subset. A query that cannot encode one conjunct fails as a whole: a partial script would answer sat or unsat about conditions it does not hold.

View Source 
var ErrSolverProcess = errors.New("the SMT solver did not answer")

ErrSolverProcess is returned when a solver was found but did not answer: it crashed, failed, or replied unintelligibly. Never a verdict, not even `unknown`.

View Source 
var ErrUnsupportedCapability = errors.New("the SMT solver does not support a feature this query needs")

ErrUnsupportedCapability is returned when the backend found lacks a feature the query needs. It is a refusal, not a verdict: nothing is degraded and no answer is guessed from a script the backend would not accept.

Functions

func CoreLabel 

func CoreLabel(i int) string

CoreLabel names the assertion at index i in a labelled script. The index is the label, so a label a solver returns reads back the Assertion itself, with the provenance it carries, rather than a table kept beside the query.

func CoreScript 

func CoreScript(q *Query, include []int) string

CoreScript renders the query as a core-producing script: every assertion labelled, unsat cores turned on, and `get-unsat-core` asked after `check-sat`, so running the script by hand answers what the driver asks. include, when non-nil, asserts only the assertions at those indices, which is how a core is reduced without retranslating.

func Fixed 

func Fixed(ctx *runtime.Context, sym *symbols.Symbol, inst *runtime.Instance) ([]Pin, []Unfixed)

Fixed reads the values the model already fixes for the features of sym: what inst holds where an object was created, else what the declaration states. The values are read through the evaluator, which is what a verdict about them reads, rather than through a second reader of the same declarations.

The second result names the features whose value could not be read, which stay free rather than being reported as fixed to something.

func FixedFor 

func FixedFor(ctx *runtime.Context, f Fixing) ([]Pin, []Unfixed)

FixedFor gathers the values fixed for a query about the fixing's element: what its object holds for the features of its own definition, else what the owner — the element the conditions were written in — declares, and then what the element's own features declare. A feature fixed twice is fixed by the nearer source, which is what an evaluation about it would read.

func MaxConfigurationsFromEnv 

func MaxConfigurationsFromEnv() int

MaxConfigurationsFromEnv is the bound the environment asks enumeration to use, or DefaultMaxConfigurations when it names none or names an unusable one: a bound is what stops a runaway, so an unreadable override never removes it.

func Script 

func Script(q *Query) string

Script renders the query as an SMT-LIB2 script: its logic, declarations, assertions each preceded by a comment naming where it came from, and `check-sat`. Output is deterministic, so it compares byte for byte.

func Unsupported 

func Unsupported(err error) bool

Unsupported reports whether the error is a backend refusing a capability, which is a reported refusal rather than a defect in the script.

func Write 

func Write(w io.Writer, q *Query) error

Write writes the query's script to w.

Types

type Assertion 

type Assertion struct {
	// Term is the boolean term asserted.
	Term *Term

	// From records the condition the term encodes.
	From Provenance
}

Assertion is one term the query asserts, with where it came from.

type Assignment 

type Assignment struct {
	// Var is the variable the solver assigned, naming the feature it stands for.
	Var *Var

	// Value renders the value as the notation writes it: a quantity with its
	// unit, an enumeration value by name, a number, a boolean or a string.
	Value string

	// Raw is the solver's own S-expression for the value.
	Raw string

	// Rendered is false when the solver answered with a term the notation has no
	// literal for, such as an algebraic number, and Value repeats Raw.
	Rendered bool
}

Assignment is one variable's value in a satisfying model, rendered in the notation's own terms rather than SMT-LIB's.

type Capabilities 

type Capabilities struct {
	// Solver names the backend the answers are about.
	Solver string

	// Probed reports that the answers came from running the executable rather
	// than from a declaration.
	Probed bool

	// Elapsed is how long probing took, zero for declared capabilities.
	Elapsed time.Duration
	// contains filtered or unexported fields
}

Capabilities is what one backend supports of the subset this layer needs, either probed by running it or declared for a backend already known.

func DeclaredCapabilities 

func DeclaredCapabilities(solver string, supported ...Capability) *Capabilities

DeclaredCapabilities states what a backend supports without probing it, which is how a caller that already knows a backend avoids the probe.

func (*Capabilities) Detail 

func (c *Capabilities) Detail(capability Capability) string

Detail is what the backend said when it refused the capability or left the check undecided, empty for one it supports.

func (*Capabilities) Missing 

func (c *Capabilities) Missing(needed []Capability) []Capability

Missing are those of the capabilities the backend refused, in the order given, with duplicates dropped.

func (*Capabilities) Refuses 

func (c *Capabilities) Refuses(capability Capability) bool

Refuses reports whether the backend rejected the capability. Only a refusal stops a query: a check that settled nothing does not.

func (*Capabilities) Supported 

func (c *Capabilities) Supported() []Capability

Supported are the capabilities the backend has, in AllCapabilities order.

func (*Capabilities) Supports 

func (c *Capabilities) Supports(capability Capability) bool

Supports reports whether the backend was found to have the capability.

func (*Capabilities) Undetermined 

func (c *Capabilities) Undetermined(capability Capability) bool

Undetermined reports that the check neither established the capability nor was refused, so what the backend does with the feature is unknown.

type Capability 

type Capability int

Capability is one thing this layer needs of a backend beyond parsing SMT-LIB2: a theory feature, a script-level facility, or a solver's own extension. 

const (
	// CapModels is `:produce-models` with `(get-value …)`, which every answer
	// carrying an assignment needs.
	CapModels Capability = iota
	// CapUnsatCores is `:produce-unsat-cores` with `:named` assertions and
	// `(get-unsat-core)`, which explaining a conflict needs.
	CapUnsatCores
	// CapIncremental is more than one `(check-sat)` in one dialogue, which
	// enumerating configurations needs.
	CapIncremental
	// CapDatatypes is `(declare-datatypes …)` with nullary constructors, which
	// enumerations and variation points are declared as.
	CapDatatypes
	// CapStrings is the String sort with equality, from the strings theory.
	CapStrings
	// CapIntegerDivision is `div` and `mod` from the Ints theory.
	CapIntegerDivision
	// CapNonlinearArith is a product or quotient of two non-literal terms.
	CapNonlinearArith
	// CapMixedArith is the mixed integer and real logics AUFLIRA and AUFNIRA,
	// which a query over both Int and Real is set to.
	CapMixedArith
	// CapNonStandardLogic is `(set-logic ALL)`, which no SMT-LIB logic name
	// covers and which datatypes and strings are set to.
	CapNonStandardLogic
	// CapOptimization is `(maximize …)`/`(minimize …)` with `(get-objectives)`,
	// a solver extension rather than SMT-LIB 2.6.
	CapOptimization
	// CapOptimizationPriority is `:opt.priority`, a z3 extension for ordering
	// several objectives.
	CapOptimizationPriority
)

func (Capability) Feature 

func (c Capability) Feature() string

Feature says what SMT-LIB feature, or which extension, the capability is.

func (Capability) String 

func (c Capability) String() string

String names the capability as a report names it.

type Core 

type Core struct {
	// Members are the conflicting assertions, in the query's assertion order.
	Members []Assertion

	// Indices are the positions those assertions hold in Query.Assertions.
	Indices []int

	// Minimal reports that dropping any one member was tried and left the rest
	// satisfiable, so every member is needed. It is false for a core reported as
	// the solver produced it, which is unsatisfiable but not necessarily
	// irreducible.
	Minimal bool

	// Note says why minimality was not established, empty when it was.
	Note string

	// Rounds is how many further solver calls reduction made.
	Rounds int

	// Elapsed is how long reduction took.
	Elapsed time.Duration
}

Core is a set of assertions whose conjunction is unsatisfiable: the conditions that conflict, each carrying the provenance of the condition it came from.

type CoreError 

type CoreError struct {
	// Solver is the executable that was run.
	Solver string

	// Detail says what it answered instead of a core.
	Detail string

	// Stderr is what the solver wrote on standard error, trimmed.
	Stderr string
}

CoreError says which solver would not explain its unsat verdict and how. It unwraps to both ErrNoCore and ErrSolverProcess, as the solver did not answer what it was asked.

func (*CoreError) Error 

func (e *CoreError) Error() string

Error reports the failure, naming the solver and what it answered.

func (*CoreError) Unwrap 

func (e *CoreError) Unwrap() []error

Unwrap returns both kinds this failure is, so either is testable with errors.Is.

type Direction 

type Direction int

Direction is the way an objective's value is to be improved. 

const (
	// Minimize asks for the least value the conditions permit.
	Minimize Direction = iota
	// Maximize asks for the greatest value the conditions permit.
	Maximize
)

func (Direction) String 

func (d Direction) String() string

String names the direction as the emitted objective form reads.

type Features 

type Features struct {
	// Bool, Int, Real, Strings and Datatypes are set for each sort used, by a
	// declared variable or by a term.
	Bool      bool
	Int       bool
	Real      bool
	Strings   bool
	Datatypes bool

	// Nonlinear is set when a product or a quotient of two non-literal terms is
	// asserted, which no linear logic admits.
	Nonlinear bool

	// IntegerDivision is set when `div` or `mod` from the Ints theory is used.
	// By a literal divisor this stays linear; by a computed one it is nonlinear.
	IntegerDivision bool
}

Features is what a query uses of SMT-LIB: the sorts its variables and terms range over, and the arithmetic its terms apply.

type Fixing 

type Fixing struct {
	Element    *symbols.Symbol
	Owner      *symbols.Symbol
	Object     *runtime.Instance
	ObjectType *symbols.Symbol
}

Fixing is what a query reads fixed values from: the element it is about, the element whose declarations its conditions were written among, and the object a verdict about it would be about, named by the definition this resolution declares — an object carried over a submission is bound to symbols of another scope tree, which are not the ones the query is translated from.

type LogicChoice 

type LogicChoice struct {
	// Name is the logic as `set-logic` names it.
	Name string

	// Standard reports that the SMT-LIB 2.6 logic list defines Name. It is false
	// only for NonStandardLogic.
	Standard bool

	// Why names the features that forced this logic, for the script's comment
	// and for a message about a solver that refuses it.
	Why string
}

LogicChoice is the logic a script sets: its name, whether SMT-LIB defines it, and what the query uses that forced it.

type NoObjectiveError 

type NoObjectiveError struct {
	// Element names the analysis case asked about.
	Element string
}

NoObjectiveError says which analysis case states no objective. It unwraps to ErrNoObjective.

func (*NoObjectiveError) Error 

func (e *NoObjectiveError) Error() string

Error reports that the case states no objective.

func (*NoObjectiveError) Unwrap 

func (e *NoObjectiveError) Unwrap() error

Unwrap returns ErrNoObjective.

type NoOptimizationError 

type NoOptimizationError struct {
	// Solver is the executable that was run.
	Solver string

	// Detail says how it turned out not to implement optimization.
	Detail string

	// Cause is the capability refusal this was settled by, when one settled it.
	Cause error
}

NoOptimizationError names the solver that does not implement optimization and what to run instead. It unwraps to ErrNoOptimization.

func (*NoOptimizationError) Error 

func (e *NoOptimizationError) Error() string

Error reports that the solver cannot optimize, naming what can.

func (*NoOptimizationError) Unwrap 

func (e *NoOptimizationError) Unwrap() []error

Unwrap returns ErrNoOptimization, and the capability refusal behind it when the capability model settled it.

type NoSolverError 

type NoSolverError struct {
	// Override is the value of the OPENSYSML_SMT override, empty when unset.
	Override string

	// Looked lists the executables looked for on PATH, in order.
	Looked []string
}

NoSolverError names the candidates looked for and what to install. It unwraps to ErrNoSolver.

func (*NoSolverError) Error 

func (e *NoSolverError) Error() string

Error reports that no solver was found, naming what would satisfy the search.

func (*NoSolverError) Unwrap 

func (e *NoSolverError) Unwrap() error

Unwrap returns ErrNoSolver.

type NoVariationsError 

type NoVariationsError struct {
	// Kind and Element name the element asked about.
	Kind    string
	Element string
}

NoVariationsError says which element reads no variation point. It unwraps to ErrNoVariations.

func (*NoVariationsError) Error 

func (e *NoVariationsError) Error() string

Error reports that the element's conditions read no variation point.

func (*NoVariationsError) Unwrap 

func (e *NoVariationsError) Unwrap() error

Unwrap returns ErrNoVariations.

type NotTranslatableError 

type NotTranslatableError struct {
	// Construct names the construct that refused, as the notation writes it.
	Construct string

	// Reason says why it is outside the subset.
	Reason string

	// Element is the element whose condition was being translated.
	Element string

	// Condition is the condition as written, empty when the refusal is about a
	// declaration rather than a condition.
	Condition string

	// File is the document the construct was written in, empty when unknown.
	File string

	// Span is where in File it was written.
	Span source.Span

	// Location renders File and Span as `file:line:col`, empty when unknown.
	Location string
}

NotTranslatableError says which construct refused, why, and where it was written. It unwraps to ErrNotTranslatable.

func (*NotTranslatableError) Error 

func (e *NotTranslatableError) Error() string

Error reports the refusal, naming the construct, the condition it appeared in, and where it was written.

func (*NotTranslatableError) Unwrap 

func (e *NotTranslatableError) Unwrap() error

Unwrap returns ErrNotTranslatable, so a caller tests the kind of failure rather than its text.

type Objective 

type Objective struct {
	// Direction is the way its value is to be improved.
	Direction Direction

	// Term is the translated objective expression, of an arithmetic sort.
	Term *Term

	// Name is the objective's name as the model wrote it, empty for an anonymous
	// one.
	Name string

	// Symbol is the objective usage it came from.
	Symbol *symbols.Symbol

	// Expression is the objective expression as written.
	Expression string

	// Dimension is the quantity dimension its value is expressed in over base
	// units, empty for a value that has none.
	Dimension string

	// Unit names the base units its magnitude is expressed in ("g", "m·s^-1"),
	// empty when the value is no quantity or no quantity named them.
	Unit string

	// File and Span are where the objective was written.
	File string
	Span source.Span

	// Location renders File and Span as `file:line:col`.
	Location string
}

Objective is one objective a query optimizes: which way its value is to be improved, the term stating that value, and where the objective was written.

type ObjectiveError 

type ObjectiveError struct {
	// Objective names the objective as the model writes it.
	Objective string

	// Reason says what about it cannot be optimized.
	Reason string

	// Remedy says what the model would have to state instead, empty when there
	// is nothing to suggest.
	Remedy string

	// Element is the analysis case stating the objective.
	Element string

	// File is the document it was written in, empty when unknown.
	File string

	// Span is where in File it was written.
	Span source.Span

	// Location renders File and Span as `file:line:col`, empty when unknown.
	Location string
}

ObjectiveError says which objective cannot be optimized, why, and where it was written. It unwraps to ErrNotOptimizable.

func (*ObjectiveError) Error 

func (e *ObjectiveError) Error() string

Error reports the refusal, naming the objective and where it was written.

func (*ObjectiveError) Unwrap 

func (e *ObjectiveError) Unwrap() error

Unwrap returns ErrNotOptimizable.

type Op 

type Op int

Op is the operator a term applies. The set is closed: every translatable construct maps onto one of these, and anything else refuses with ErrNotTranslatable. 

const (
	// OpBool is a boolean literal, held in Bool.
	OpBool Op = iota
	// OpInt is an integer literal, held in Int.
	OpInt
	// OpReal is a real literal, held as an exact rational in Real.
	OpReal
	// OpString is a string literal, held in Str.
	OpString
	// OpValue is a value of a datatype sort — an enumeration literal or a
	// variant — named by Str.
	OpValue
	// OpVar is a variable, held in Var.
	OpVar

	// OpNot is boolean negation, one argument.
	OpNot
	// OpAnd is conjunction, two or more arguments.
	OpAnd
	// OpOr is disjunction, two or more arguments.
	OpOr
	// OpXor is exclusive disjunction, two arguments.
	OpXor
	// OpImplies is implication, two arguments.
	OpImplies

	// OpEq is equality of two terms of the same sort.
	OpEq
	// OpNe is inequality of two terms of the same sort.
	OpNe
	// OpLt is `<` between two numbers of the same sort.
	OpLt
	// OpLe is `<=` between two numbers of the same sort.
	OpLe
	// OpGt is `>` between two numbers of the same sort.
	OpGt
	// OpGe is `>=` between two numbers of the same sort.
	OpGe

	// OpAdd is addition of two numbers of the same sort.
	OpAdd
	// OpSub is subtraction of two numbers of the same sort.
	OpSub
	// OpMul is multiplication of two numbers of the same sort.
	OpMul
	// OpDiv is division of two reals.
	OpDiv
	// OpIntDiv is SMT-LIB's Euclidean integer division; TruncDiv builds the
	// evaluator's truncating division from it.
	OpIntDiv
	// OpNeg is arithmetic negation, one argument.
	OpNeg

	// OpIte is `if c then a else b`: a boolean condition and two branches of
	// the same sort.
	OpIte
	// OpToReal widens an integer term to a real one.
	OpToReal
)

type Optimum 

type Optimum struct {
	// Objective is the objective asked about.
	Objective Objective

	// Status says what came of asking.
	Status OptimumStatus

	// Value is the optimum in the notation's own terms, with the units its
	// magnitude is expressed in; empty unless Status is OptimumAttained.
	Value string

	// Bound is the value the objective approaches without attaining it, in the
	// notation's own terms; empty unless Status is OptimumBounded.
	Bound string

	// Feasible is a value the reported model attains, in the notation's own
	// terms: a witness the conditions permit, not an optimum.
	Feasible string

	// Raw is the solver's own expression for the optimum.
	Raw string

	// Detail says why an optimum was not reported, empty when one was.
	Detail string
}

Optimum is what a solver answered about one objective.

type OptimumError 

type OptimumError struct {
	// Solver is the executable that was run.
	Solver string

	// Objective names the objective it was asked about.
	Objective string

	// Detail says what it answered instead of an optimum.
	Detail string

	// Stderr is what the solver wrote on standard error, trimmed.
	Stderr string
}

OptimumError says which solver would not report an optimum it had found, and how. It unwraps to both ErrNoOptimum and ErrSolverProcess, as the solver did not answer what it was asked.

func (*OptimumError) Error 

func (e *OptimumError) Error() string

Error reports the failure, naming the solver and what it answered.

func (*OptimumError) Unwrap 

func (e *OptimumError) Unwrap() []error

Unwrap returns both kinds this failure is, so either is testable with errors.Is.

type OptimumStatus 

type OptimumStatus int

OptimumStatus is what came of asking for one objective's optimum. The cases stay distinct: a bound no assignment attains is never reported as a value, and an answer that did not survive verification is never reported as an optimum. 

const (
	// OptimumAttained means the value reported is the optimum and an assignment
	// attains it, both checked here rather than taken on the solver's word.
	OptimumAttained OptimumStatus = iota

	// OptimumBounded means the objective approaches a bound no assignment
	// attains, which is what a solver reports as an infinitesimal or an interval.
	OptimumBounded

	// OptimumUnbounded means the conditions permit arbitrarily better values, so
	// there is no optimum to report.
	OptimumUnbounded

	// OptimumUnverified means the solver reported an optimum that verification
	// refuted: a better value is feasible. Only the feasible value found stands.
	OptimumUnverified

	// OptimumUndecided means verification itself was not decided, so whether the
	// value reported is the optimum is unknown.
	OptimumUndecided
)

func (OptimumStatus) String 

func (s OptimumStatus) String() string

String names the outcome in the terms a report uses.

type Pin 

type Pin struct {
	// Feature is the feature declaration whose value is fixed.
	Feature *symbols.Symbol

	// Name is the feature as the element naming it writes it.
	Name string

	// Value is the value it is fixed to, read where the evaluator reads it.
	Value runtime.Value

	// Source says where the value came from.
	Source PinSource

	// Object is the object holding the value, 0 for a value no object holds.
	Object int64
}

Pin fixes one feature to a value a query asserts, rather than leaving the feature free for the solver to choose.

type PinError 

type PinError struct {
	// Feature names the feature whose value was to be fixed.
	Feature string

	// Value renders the value as the notation writes it.
	Value string

	// Reason says why it cannot be fixed.
	Reason string

	// Source says where the value came from.
	Source PinSource

	// File and Span are where the feature was declared.
	File string
	Span source.Span

	// Location renders File and Span as `file:line:col`, empty when unknown.
	Location string
}

PinError says which value could not be fixed, why, and where the feature was declared. It unwraps to ErrNotPinnable.

func (*PinError) Error 

func (e *PinError) Error() string

Error reports the refusal, naming the feature, the value and where it was declared.

func (*PinError) Unwrap 

func (e *PinError) Unwrap() error

Unwrap returns ErrNotPinnable, so a caller tests the kind of failure rather than its text.

type PinSource 

type PinSource int

PinSource says where a fixed value came from, so a report distinguishes what an object holds from what the model declares and from what a caller chose. 

const (
	// PinHeld is a value an object holds.
	PinHeld PinSource = iota
	// PinDeclared is a value the model declares for a feature.
	PinDeclared
	// PinChosen is a value the caller supplied, such as a variant selection.
	PinChosen
)

func (PinSource) String 

func (s PinSource) String() string

String names the source for a report a machine reads.

type PinnedValue 

type PinnedValue struct {
	// Var is the variable fixed.
	Var *Var

	// Value renders the fixed value as the notation writes it.
	Value string

	// Source says where the value came from.
	Source PinSource

	// Object is the object holding the value, 0 for a value no object holds.
	Object int64

	// Index is the assertion's position in Query.Assertions.
	Index int
}

PinnedValue is a pin the query asserts: the variable it fixed, the value as the notation writes it, and where that assertion sits, so an unsat core naming the assertion names the pin.

type Provenance 

type Provenance struct {
	// Kind is the kind of element the assertion came from: "constraint",
	// "requirement", "satisfaction", or "declaration" for a domain assertion.
	Kind string

	// Element names that element as a verdict about it would.
	Element string

	// Condition is the condition as written, negation and grouping included.
	Condition string

	// Role says why the query asserts the term.
	Role Role

	// Declared is the element that declared the condition, which is the
	// supertype it was inherited from for an inherited one.
	Declared *symbols.Symbol

	// File and Span are where the condition was written.
	File string
	Span source.Span

	// Location renders File and Span as `file:line:col`.
	Location string
}

Provenance records what an assertion came from, so a later step can map an answer about the script back to what the user wrote.

type Query 

type Query struct {
	// Kind is the kind of element translated: "constraint", "requirement" or
	// "satisfaction".
	Kind string

	// Element names the translated element as a verdict about it would.
	Element string

	// Negated is set for an element asserting that its conditions do not all
	// hold (`assert not …`), which the query asserts as one denial.
	Negated bool

	// Sorts are the datatype sorts the query declares, ordered by name.
	Sorts []Sort

	// Vars are the variables the query declares, ordered by name.
	Vars []*Var

	// Assertions are the terms asserted: declared domains first, then the
	// well-definedness side conditions, then the conditions in the order the
	// evaluator checks them.
	Assertions []Assertion

	// Nonlinear is set when a product or a quotient of two non-literal terms was
	// asserted, which is what a nonlinear logic is set for.
	Nonlinear bool

	// IntegerDivision is set when integer division or remainder was encoded,
	// which needs `div` and `mod` from the Ints theory of a backend.
	IntegerDivision bool

	// Pinned are the values the query fixes rather than leaves free, each naming
	// the assertion that fixes it; nil for a query that fixes none.
	Pinned []PinnedValue

	// Unread are the values that were to be fixed but that no variable of the
	// query reads, reported rather than dropped.
	Unread []Unread

	// Objectives are the objectives to optimize, in the order the analysis case
	// declares them, which is the order they are optimized in; nil for a query
	// that only asks about satisfiability.
	Objectives []Objective
}

Query is a translated element: the variables its conditions read, the finite sorts they range over, and the terms it asserts. It is what a solver-facing step consumes, and what the SMT-LIB2 writer writes.

func Analysis 

func Analysis(ctx *runtime.Context, sym *symbols.Symbol, scope *symbols.Scope) (*Query, error)

Analysis translates an analysis case as an optimization query: what its conditions permit, and the objectives to improve within that.

The contract, which SysML v2 leaves to a tool since it defines no solving: direction comes from the trade-study definition the objective is typed by (TradeStudies::MinimizeObjective or MaximizeObjective), the value to improve from the expression the objective states for the library's `best` feature (`attribute :>> best = expression;`), and what is feasible from the conditions the case requires or assumes together with the ones each objective states in its own body.

func AnalysisWith 

func AnalysisWith(ctx *runtime.Context, sym *symbols.Symbol, scope *symbols.Scope, pins []Pin) (*Query, error)

AnalysisWith translates an analysis case with values already fixed, so the optimum is the best one consistent with what the model already fixes. With no pins it is Analysis.

func Constraint 

func Constraint(ctx *runtime.Context, sym *symbols.Symbol, scope *symbols.Scope) (*Query, error)

Constraint translates the conditions sym states as a constraint, inherited ones included, in the order the evaluator checks them. scope stands in for sym's own scope when sym declares none.

func ConstraintWith 

func ConstraintWith(ctx *runtime.Context, sym *symbols.Symbol, scope *symbols.Scope, pins []Pin) (*Query, error)

ConstraintWith translates a constraint with values already fixed, so the solver synthesises only what the model leaves free. With no pins it is Constraint.

func Requirement 

func Requirement(ctx *runtime.Context, sym *symbols.Symbol, scope *symbols.Scope) (*Query, error)

Requirement translates the conditions sym states as a requirement, its assumptions included as assumed rather than required.

func RequirementWith 

func RequirementWith(ctx *runtime.Context, sym *symbols.Symbol, scope *symbols.Scope, pins []Pin) (*Query, error)

RequirementWith translates a requirement with values already fixed. With no pins it is Requirement.

func Satisfaction 

func Satisfaction(ctx *runtime.Context, assertion *runtime.SatisfyAssertion) (*Query, error)

Satisfaction translates the conditions an `assert satisfy` checks: those of the requirement it names, read through that requirement's own parameters, since the query asks what they permit rather than what the subject holds.

func SatisfactionWith 

func SatisfactionWith(ctx *runtime.Context, assertion *runtime.SatisfyAssertion, pins []Pin) (*Query, error)

SatisfactionWith translates an `assert satisfy` with values already fixed. With no pins it is Satisfaction.

func Translate 

func Translate(ctx *runtime.Context, subject Subject, conds []runtime.Condition) (*Query, error)

Translate builds a query from conditions the runtime collected. One refusal fails the whole translation, since a query missing a conjunct would answer about conditions it does not hold.

func TranslateWith 

func TranslateWith(ctx *runtime.Context, subject Subject, conds []runtime.Condition, pins []Pin) (*Query, error)

TranslateWith builds a query whose pinned features are asserted equal to the values given, leaving the rest free. A value that cannot be fixed refuses, as an untranslatable condition does; a value no condition reads is reported in Query.Unread rather than dropped.

func (*Query) Features 

func (q *Query) Features() Features

Features inventories what the query uses, reading its terms rather than trusting the flags a translation recorded, so a hand-built query inventories the same.

func (*Query) FixValue 

func (q *Query) FixValue(v *Var, value string, src PinSource) error

FixValue fixes a variable of a finite sort to one of that sort's values, naming a variant or an enumeration literal by its qualified name, as a caller choosing a configuration to check does. The assertion is appended, so the positions the query's other assertions hold — and any core naming them — do not move.

func (*Query) Fixes 

func (q *Query) Fixes() bool

Fixes reports whether the query fixes any value, which is what makes an unsat verdict about it a verdict about those values too.

func (*Query) Free 

func (q *Query) Free() []*Var

Free are the variables the query leaves for the solver to choose, in the order they are declared.

func (*Query) Logic 

func (q *Query) Logic() string

Logic is the name the script's `set-logic` sets.

func (*Query) LogicChoice 

func (q *Query) LogicChoice() LogicChoice

LogicChoice names the narrowest SMT-LIB logic that covers what the query uses, falling back to NonStandardLogic only for features the logic list has no logic for. Names are the SMT-LIB 2.6 list's own; nothing is widened to avoid a hard case, and a wider logic than the terms need is never set.

func (*Query) Optimizes 

func (q *Query) Optimizes() bool

Optimizes reports whether the query asks for an optimum rather than only for satisfiability.

func (*Query) Requires 

func (q *Query) Requires() []Capability

Requires are the capabilities a backend must have to answer this query: what its sorts and operators use, and the non-standard logic when it needs one. Capabilities an operation adds — a model, an unsat core — are the operation's.

func (*Query) Variations 

func (q *Query) Variations() []*Var

Variations are the variables standing for the variation points the query's conditions read, in declaration order. They are the variables a configuration assigns.

type Result 

type Result struct {
	// Query is the query asked.
	Query *Query

	// Status is the verdict.
	Status Status

	// Solver names the solver that answered.
	Solver string

	// TimedOut reports that the solver ran out of time rather than giving up:
	// Status is StatusUnknown, or StatusSat and Undecided for an enumeration
	// reporting what it had found when the deadline fired.
	TimedOut bool

	// Reason is what the solver said when asked why it answered `unknown`,
	// empty when it said nothing or was not asked.
	Reason string

	// Model is the satisfying assignment, one entry per declared variable, for
	// StatusSat and empty otherwise. A solver may answer with any model of many:
	// it is one witness, not a canonical answer.
	Model []Assignment

	// Solutions are the distinct assignments an enumeration reported, in the
	// order the solver produced them, over the variables enumerated rather than
	// every declared one; nil for a plain solve.
	Solutions [][]Assignment

	// Truncated reports that an enumeration stopped before it had shown there is
	// no further solution, for the reason AtBound or Undecided names.
	Truncated bool

	// AtBound reports that the enumeration stopped because it had reported as
	// many solutions as it was asked for; raising the bound may report more.
	AtBound bool

	// Undecided reports that the enumeration stopped because the solver stopped
	// deciding or ran out of time (TimedOut), whether or not it said why: the
	// solutions found stand, and whether others exist is unknown.
	Undecided bool

	// Optima are what came of asking for each objective's optimum, in the order
	// they are optimized; nil for a query that states none.
	Optima []Optimum

	// Core holds the conflicting assertions for a query Explain found unsat, and
	// is nil for every other verdict and for a plain Solve.
	Core *Core

	// Elapsed is how long the solver took, for an Explain every round of
	// shrinking the core included.
	Elapsed time.Duration
}

Result is what a solver answered about one query.

func Configurations 

func Configurations(ctx context.Context, q *Query, limit int) (*Result, error)

Configurations enumerates the combinations of variants that satisfy the query, asking for at most limit of them; a limit of zero or less uses the bound the environment names. Each combination is found by its own `check-sat`, with the combinations already reported denied, and Result.Truncated says the enumeration stopped at its bound rather than having shown there is no other.

func Explain 

func Explain(ctx context.Context, q *Query) (*Result, error)

Explain discovers a solver and asks it to explain the query.

func Optimize 

func Optimize(ctx context.Context, q *Query) (*Result, error)

Optimize discovers a solver and asks it for the query's optima.

func Solve 

func Solve(ctx context.Context, q *Query) (*Result, error)

Solve discovers a solver and asks it about the query.

type Role 

type Role int

Role says why a query asserts a term. 

const (
	// RoleRequired is a condition the element requires to hold (`require`,
	// `assert`).
	RoleRequired Role = iota
	// RoleAssumed is a condition the element assumes (`assume`), trusted rather
	// than required.
	RoleAssumed
	// RoleDenied is the assertion a negated element makes: that its required
	// conditions do not all hold.
	RoleDenied
	// RoleDomain is a bound a declaration puts on a variable's values rather
	// than a condition the model wrote, such as a Natural being non-negative.
	RoleDomain
	// RoleDefined is a side condition a condition needs for the solver to mean by
	// it what the evaluator means, such as a divisor being non-zero.
	RoleDefined
	// RolePinned is a value the model already fixes — held by an object, declared
	// by the model, or chosen by the caller — asserted so the solver synthesises
	// only what is still free.
	RolePinned
	// RoleExcluded is an assignment already reported, denied so enumerating asks
	// for a different one.
	RoleExcluded
)

func (Role) String 

func (r Role) String() string

String names the role as an assertion's comment reads it.

type Solver 

type Solver struct {
	// Name is the solver as a message names it, its executable's base name.
	Name string

	// Path is the executable run.
	Path string

	// Args are the arguments that put it in SMT-LIB2 mode on standard input.
	Args []string

	// Timeout is how long it is given to answer one query; zero means
	// DefaultTimeout.
	Timeout time.Duration

	// Env are environment variables added to the process's own environment.
	Env []string

	// CoreBudget is how long shrinking an unsat core is given in total; zero
	// means the OPENSYSML_SMT_CORE_BUDGET override or DefaultCoreBudget.
	CoreBudget time.Duration

	// MaxCoreMembers is the largest core shrinking is attempted over; zero means
	// DefaultMaxCoreMembers.
	MaxCoreMembers int

	// Declared states what this backend supports instead of probing it, which is
	// how a caller that already knows a backend skips the probe; nil probes.
	Declared *Capabilities
}

Solver is an external SMT solver run as a process: no library is linked in, so releases stay pure Go and cross-compile.

func Discover 

func Discover() (*Solver, error)

Discover finds a solver: the OPENSYSML_SMT override first, then z3 and cvc5 on PATH. An absent solver is a typed error, never a fabricated verdict.

func (*Solver) Capabilities 

func (s *Solver) Capabilities(ctx context.Context) (*Capabilities, error)

Capabilities reports what this backend supports of the whole subset, probing each capability once per executable however many queries ask. Declared capabilities are returned as they are, unprobed.

func (*Solver) Configurations 

func (s *Solver) Configurations(ctx context.Context, q *Query, limit int) (*Result, error)

Configurations enumerates satisfying combinations of variants with this solver.

func (*Solver) Explain 

func (s *Solver) Explain(ctx context.Context, q *Query) (*Result, error)

Explain asks the solver about the query and, when the verdict is unsat, for the assertions that conflict: the solver's own unsat core, shrunk to a minimal one while the budget lasts. sat and unknown carry no core, and a solver that refuses cores or names an assertion the query did not assert is an error rather than an empty or invented core.

func (*Solver) Optimize 

func (s *Solver) Optimize(ctx context.Context, q *Query) (*Result, error)

Optimize asks the solver for the optimum of each objective, in the lexicographic order the query declares them.

Optimization is a z3 extension rather than SMT-LIB, so a backend without it is reported rather than degraded to a plain satisfiability check, and every optimum a backend does report is verified here: that an assignment attains it, and that no assignment does lexicographically better. A solver whose answer fails either check reports no optimum, only the feasible value it found.

func (*Solver) Solve 

func (s *Solver) Solve(ctx context.Context, q *Query) (*Result, error)

Solve writes the query's script to the solver and reads its verdict, plus the model on `sat`. Failing to obtain a verdict is an error, not `unknown`, and a backend lacking a feature the query needs refuses before it is run.

type SolverProcessError 

type SolverProcessError struct {
	// Solver is the executable that was run.
	Solver string

	// Stage names what was being done: "start", "write", "check-sat",
	// "get-value", "capability check" or "exit".
	Stage string

	// Detail says what went wrong.
	Detail string

	// Stderr is what the solver wrote on standard error, trimmed.
	Stderr string

	// Err is the underlying error, nil when the failure was the reply itself.
	Err error
}

SolverProcessError says which solver failed, at which step, and what it wrote on standard error. It unwraps to ErrSolverProcess.

func (*SolverProcessError) Error 

func (e *SolverProcessError) Error() string

Error reports the failure, naming the solver and the step it failed at.

func (*SolverProcessError) Unwrap 

func (e *SolverProcessError) Unwrap() []error

Unwrap returns ErrSolverProcess, and the underlying error when there is one, so both are testable with errors.Is.

type Sort 

type Sort struct {
	// Kind is which kind of sort this is.
	Kind SortKind

	// Name is the sort's SMT-LIB name, unquoted: "Bool", "Int", "Real",
	// "String", or the qualified name of the definition a datatype comes from.
	Name string

	// Values are a datatype's constructors, in declaration order, unquoted; nil
	// for a scalar sort.
	Values []string

	// Origin is the enumeration definition or variation point a datatype sort
	// was declared for; nil for a scalar sort.
	Origin string

	// Variation marks a datatype sort declared for a variation point, whose
	// values are its variants rather than an enumeration's literals.
	Variation bool
}

Sort is the sort of a term: one of the four scalar sorts, or a finite datatype declared by the query.

func (Sort) Equal 

func (s Sort) Equal(other Sort) bool

Equal reports whether two sorts are the same sort.

func (Sort) Numeric 

func (s Sort) Numeric() bool

Numeric reports whether the sort is Int or Real.

func (Sort) String 

func (s Sort) String() string

String returns the sort as it is written in a script.

type SortKind 

type SortKind int

SortKind is the kind of value a sort holds. The set is closed: a construct whose values fit none of these kinds is not translatable. 

const (
	// SortBool is the boolean sort, SMT-LIB Bool.
	SortBool SortKind = iota
	// SortInt is the integer sort, SMT-LIB Int.
	SortInt
	// SortReal is the real sort, SMT-LIB Real.
	SortReal
	// SortString is the string sort, SMT-LIB String.
	SortString
	// SortDatatype is a finite enumerated sort, declared as an SMT-LIB datatype
	// with one nullary constructor per value: an enumeration definition's
	// literals, or a variation point's variants.
	SortDatatype
)

type Status 

type Status int

Status is a solver's verdict about a query. The three verdicts stay distinct: StatusUnknown is never reported as either of the others. 

const (
	// StatusSat means the solver found an assignment satisfying the assertions.
	StatusSat Status = iota
	// StatusUnsat means no assignment satisfies them.
	StatusUnsat
	// StatusUnknown means the solver did not decide: it timed out, or gave up on
	// arithmetic it cannot decide.
	StatusUnknown
)

func (Status) String 

func (s Status) String() string

String names the verdict as SMT-LIB writes it.

type Subject 

type Subject struct {
	// Kind is the kind of element: "constraint", "requirement" or
	// "satisfaction".
	Kind string

	// Name is the element as a verdict about it would name it.
	Name string

	// Symbol is the element's declaration, used for provenance.
	Symbol *symbols.Symbol

	// Negated is set for `assert not …`, which denies the conjunction of the
	// required conditions rather than asserting each one.
	Negated bool
}

Subject is the element a query is about: what a verdict on it would name, and whether it asserts that its conditions do not hold.

type Term 

type Term struct {
	// Op is the operator applied.
	Op Op

	// Sort is the sort of the value the term yields.
	Sort Sort

	// Args are the operands of a compound term, nil for a leaf.
	Args []*Term

	// Var is the variable an OpVar term reads.
	Var *Var

	// Bool holds an OpBool literal.
	Bool bool

	// Int holds an OpInt literal.
	Int int64

	// Real holds an OpReal literal as an exact rational.
	Real *big.Rat

	// Str holds an OpString literal or the name of an OpValue datatype value.
	Str string
}

Term is one node of the query's term language: an operator, the sort of the value it yields, and its arguments. A leaf carries its value instead of arguments. Terms are built by the translator and are never mutated afterwards.

func And 

func And(args ...*Term) *Term

And returns the conjunction of boolean terms: `true` for none, the term itself for one.

func Binary 

func Binary(op Op, sort Sort, left, right *Term) *Term

Binary returns a compound term over two arguments, of the sort given.

func BoolTerm 

func BoolTerm(b bool) *Term

BoolTerm returns a boolean literal.

func IntTerm 

func IntTerm(i int64) *Term

IntTerm returns an integer literal.

func Ite 

func Ite(cond, then, otherwise *Term) *Term

Ite returns a conditional term: cond selects between two branches, which must share the sort the term yields.

func Not 

func Not(arg *Term) *Term

Not returns the negation of a boolean term, folding a double negation.

func Or 

func Or(args ...*Term) *Term

Or returns the disjunction of boolean terms: `false` for none, the term itself for one.

func RealTerm 

func RealTerm(r *big.Rat) *Term

RealTerm returns a real literal, held as the exact rational given.

func StringTerm 

func StringTerm(s string) *Term

StringTerm returns a string literal.

func ToReal 

func ToReal(arg *Term) *Term

ToReal widens an integer term to a real one, leaving a real term as it is.

func TruncDiv 

func TruncDiv(a, b *Term) *Term

TruncDiv returns integer division truncating toward zero, as the evaluator divides: `ite(a >= 0, div(a, b), -div(-a, b))`, exact for either sign of b.

func TruncRem 

func TruncRem(a, b *Term) *Term

TruncRem returns the remainder that truncating division leaves, `a - b*TruncDiv(a, b)`, which takes the sign of the dividend as `%` does.

func Unary 

func Unary(op Op, sort Sort, arg *Term) *Term

Unary returns a compound term over one argument, of the sort given.

func ValueTerm 

func ValueTerm(sort Sort, value string) *Term

ValueTerm returns a value of a datatype sort, named by one of its values.

func VarTerm 

func VarTerm(v *Var) *Term

VarTerm returns a term reading a variable.

func (*Term) Literal 

func (t *Term) Literal() bool

Literal reports whether the term is a literal value, which is what makes a product or a quotient linear.

type Unfixed 

type Unfixed struct {
	// Feature is the feature declaration whose value was not read.
	Feature *symbols.Symbol

	// Name is the feature as the element naming it writes it.
	Name string

	// Reason says why no value was read.
	Reason string
}

Unfixed is a feature whose value could not be read, so the query leaves it free. Reading a declared value is an evaluation, and one that fails says nothing about the feature.

type Unread 

type Unread struct {
	// Pin is the value that was fixed.
	Pin Pin

	// Reason says why the query does not read it.
	Reason string
}

Unread is a fixed value no variable of the query reads. It is reported rather than dropped: the query answers about the conditions, which say nothing about this feature.

type UnsupportedCapabilityError 

type UnsupportedCapabilityError struct {
	// Solver is the backend that lacks the capability.
	Solver string

	// Operation is what was being asked of it: "solving", "explaining a
	// conflict", "enumerating configurations".
	Operation string

	// Missing are the capabilities it lacks, the first being the one reported.
	Missing []Capability

	// Detail is what it answered when probed for the first missing capability.
	Detail string
}

UnsupportedCapabilityError names the backend, the features it lacks, and what was being asked of it. It unwraps to ErrUnsupportedCapability.

func (*UnsupportedCapabilityError) Error 

func (e *UnsupportedCapabilityError) Error() string

Error names the missing feature, the backend, and how to get a backend that has it, since the choice of solver is the operator's.

func (*UnsupportedCapabilityError) Unwrap 

func (e *UnsupportedCapabilityError) Unwrap() error

Unwrap returns ErrUnsupportedCapability.

type Var 

type Var struct {
	// Name is the variable's name, the qualified name of the feature it stands
	// for, with a feature chain's further steps appended with '.'.
	Name string

	// Sort is the sort of its values.
	Sort Sort

	// Symbol is the feature declaration it stands for.
	Symbol *symbols.Symbol

	// Dimension is the quantity dimension its magnitude is expressed in, over
	// base units, empty for a value that has none.
	Dimension string

	// Unit names the base units its magnitude is expressed in ("g", "m·s^-1"),
	// empty when no quantity of that dimension was written to name them.
	Unit string

	// File and Span are where the feature was declared.
	File string
	Span source.Span

	// Location renders File and Span as `file:line:col`.
	Location string
}

Var is one variable a query declares: the value a feature may take. It is unconstrained except by its sort and the domain assertions the query makes about it — values a model declares are not asserted here.

Source Files

View all Source files

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.