Solver & Routing

from jugeo.solver import Z3Session, Z3Formula, FragmentClassifier
import z3

# FragmentClassifier: inspect a formula before solving
formula = z3.And(z3.Int("x") > 0, z3.Int("x") < 100)
clf = FragmentClassifier()
fragment = clf.classify(formula)
print(fragment)          # SMTFragment.QF_LIA
print(fragment.solver)   # "z3"
print(fragment.tactics)  # ["linarith", "arith"]

# Z3Session: managed solver session with JuGeo integration
session = Z3Session(
    timeout_ms=5000,
    strategy="FRAGMENT_FIRST",
    incremental=True,
)
session.push()
session.assert_formula(formula)
result = session.check()
print(result.status)     # "UNSAT" | "SAT" | "UNKNOWN"
print(result.trust)      # TrustLevel.SOLVER if UNSAT
print(result.model)      # z3.ModelRef if SAT (counterexample)
session.pop()

# Z3Formula: wraps a z3 expression with metadata
zf = Z3Formula(
    expr=formula,
    fragment=fragment,
    source_judgment=judgment,
    label="price_bound_check",
)
print(zf.fragment)       # SMTFragment.QF_LIA
print(zf.label)          # "price_bound_check"

from jugeo.solver import SolverJurisdiction, SolverRouter, SMTFragment

# Define custom jurisdiction
jur = SolverJurisdiction(
    solver_name="z3",
    fragments=[SMTFragment.QF_LIA, SMTFragment.QF_LRA, SMTFragment.QF_BV],
    timeout_ms=10_000,
    fallback="cvc5",
)

# Router: dispatches VCs to sessions based on jurisdiction
router = SolverRouter(
    strategy="FALLBACK_CHAIN",
    jurisdictions=[jur],
)

# Route a single formula
result = router.route_and_solve(formula, label="vc_001")
print(result.solver_used)    # "z3" or "cvc5"
print(result.fragment)       # the detected fragment
print(result.escalated)      # True if escalated to fallback solver
print(result.duration_ms)    # actual solving time

# Batch routing (parallel where strategy allows)
vcs = [Z3Formula(expr=f, label=f"vc_{i}") for i, f in enumerate(formulas)]
batch_result = router.route_batch(vcs)
print(f"Verified: {batch_result.verified_count}")
print(f"Unknown : {batch_result.unknown_count}")
print(f"SAT     : {batch_result.sat_count}")  # counterexamples found

import jugeo
from jugeo.solver import SolverRouter, RoutingStrategy

# Build site and run the encoding pipeline
site = jugeo.build_site("mymod")
report = jugeo.analyze_module("mymod", property="pure")

# Access the solver results for each judgment
for j in report.judgments:
    vc = j.verification_condition
    if vc is None:
        print(f"  {j.coordinate}: no VC (trivial or FORMAL)")
        continue
    fragment = vc.fragment
    result = vc.solver_result
    print(f"  {j.coordinate}  [{fragment.name}] -> {result.status}")
    if result.status == "SAT":
        print(f"    Counterexample: {result.model_as_python_values()}")

# Configure and run the router directly
router = SolverRouter(strategy=RoutingStrategy.PORTFOLIO)
jugeo.set_solver_router(router)

# Re-run with portfolio strategy
report2 = jugeo.analyze_module("mymod", property="no_exceptions")
print(f"Closed: {report2.closed_count} / {report2.total_count}")

from jugeo.solver import FragmentClassifier, SMTFragment
import z3

clf = FragmentClassifier(verbose=True)

# A mixed-theory formula: integers + uninterpreted function
x = z3.Int("x")
f = z3.Function("f", z3.IntSort(), z3.IntSort())
formula = z3.And(x > 0, f(x) == x + 1, f(f(x)) < 100)

fragment = clf.classify(formula)
print(fragment)                   # SMTFragment.UFLIA
print(clf.classification_trace)  # step-by-step reasoning

# Check whether a formula is in a decidable fragment
print(clf.is_decidable(formula))  # True for UFLIA
print(clf.complexity_estimate(formula))  # "pspace" | "np" | "polynomial"

# Get the recommended tactics for a fragment
tactics = clf.recommended_tactics(SMTFragment.QF_AUFLIA)
print(tactics)  # ["arrays", "arith", "qfauflia"]