Enum ConcreteTerm 

pub enum ConcreteTerm {
    Var(String),
    Boolean(bool),
    String(String),
    Integer(Integer),
    Real(Real),
    BitVector(BitVector),
    Fraction {
        num: Real,
        denom: Real,
        verbatim: String,
    },
    Float(Float),
    App {
        ls: String,
        args: Vec<ConcreteTerm>,
    },
    If {
        ift: Box<ConcreteTerm>,
        then: Box<ConcreteTerm>,
        elset: Box<ConcreteTerm>,
    },
    Eps {
        var: String,
        t: Box<ConcreteTerm>,
    },
    Fun {
        args: Vec<String>,
        body: Box<ConcreteTerm>,
    },
    Quant {
        quant: String,
        vs: Vec<String>,
        t: Box<ConcreteTerm>,
    },
    Binop {
        binop: String,
        t1: Box<ConcreteTerm>,
        t2: Box<ConcreteTerm>,
    },
    Not(Box<ConcreteTerm>),
    FunctionLiteral {
        elts: Vec<FunLitElt>,
        other: Box<ConcreteTerm>,
    },
    Proj {
        name: String,
        value: Box<ConcreteTerm>,
    },
    Unknown(Value),
}

Variants

Var(String)

Boolean(bool)

String(String)

Integer(Integer)

Real(Real)

BitVector(BitVector)

Fraction

Fields

num: Real

denom: Real

verbatim: String

Float(Float)

App

Fields

ls: String

args: Vec<ConcreteTerm>

If

Fields

ift: Box<ConcreteTerm>

then: Box<ConcreteTerm>

elset: Box<ConcreteTerm>

Eps

Fields

var: String

t: Box<ConcreteTerm>

Fun

Fields

args: Vec<String>

body: Box<ConcreteTerm>

Quant

Fields

quant: String

vs: Vec<String>

t: Box<ConcreteTerm>

Binop

Fields

binop: String

t1: Box<ConcreteTerm>

t2: Box<ConcreteTerm>

Not(Box<ConcreteTerm>)

FunctionLiteral

Fields

elts: Vec<FunLitElt>

other: Box<ConcreteTerm>

Proj

Fields

name: String

value: Box<ConcreteTerm>

Unknown(Value)

Trait Implementations

impl Debug for ConcreteTerm

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.