Struct ArithmeticResolver

pub struct ArithmeticResolver {
    pub(crate) exp_map: HashMap<Sym, Exp>,
    pub(crate) pred_map: HashMap<Sym, Pred>,
}

A special resolver for integer arithmetic. It provides special predicates which evaluate integer expressions:

• is(A,B) - A=B
• isNeg(A,B) - A=-B
• isLess(A,B) - A<B
• isGreater(A,B) - A>B
• isLessEq(A,B) - A≤B
• isGreaterEq(A,B) - A≥B
• isDivider(A,B) - A mod B = 0

For all of those predicates, at least one of the arguments must be fully instantiated and must resolve to an integer value.

If the other argument also resolves to an integer, the predicate matches as expected.

is/2 and isNeg/2 accept an unbound variable as the other argument. That variable will get bound to the result of the corresponding computation.

In other cases (e.g. expression containing an unbound variable), the predicate fails. A message explaining details may be printed to the tracing log.

Expressions are represented using an integer term, or one of the following compound terms, which each take two expressions as arguments:

• add/2: addition
• sub/2: subtraction
• mul/2: multiplication
• div/2: division
• rem/2: remainder
• pow/2: power

Notably, free variables are not allowed in those expressions.

Integer overflow errors will fail the predicates.

Examples

• Computing the result of an expression and binding it to X:

  is(X, add(2, 3)).

• Comparing 4 to the result of the expression (predicate succeeds):

  is(4, mul(2, 2)).

• Comparing 4 to the result of the expression (predicate fails):

  is(4, add(1, 2)).

Fields

exp_map: HashMap<Sym, Exp>

pred_map: HashMap<Sym, Pred>

Implementations

impl ArithmeticResolver

pub fn new<T: SymbolStorage>(symbols: &mut T) -> Self

pub(crate) fn eval_exp( &self, solution: &SolutionState, exp: TermId, ) -> Option<i64>

pub(crate) fn resolve_with_args( &mut self, context: &mut ResolveContext<'_>, left: TermId, right: TermId, op: impl Fn(i64, i64) -> bool, var_generator: fn(_: i64) -> VariableSolutions, ) -> Option<Resolved<<Self as Resolver>::Choice>>

pub(crate) fn resolve_both_sides_with_args( &mut self, context: &mut ResolveContext<'_>, left: TermId, right: TermId, op: impl Fn(i64, i64) -> bool, var_generator: fn(_: i64) -> VariableSolutions, ) -> Option<Resolved<<Self as Resolver>::Choice>>

pub(crate) fn resolve_is( &mut self, args: ArgRange, context: &mut ResolveContext<'_>, ) -> Option<Resolved<<Self as Resolver>::Choice>>

pub(crate) fn resolve_neg( &mut self, args: ArgRange, context: &mut ResolveContext<'_>, ) -> Option<Resolved<<Self as Resolver>::Choice>>

pub(crate) fn resolve_instantiated_op2( &mut self, args: ArgRange, context: &mut ResolveContext<'_>, op: fn(_: i64, _: i64) -> bool, ) -> Option<Resolved<<Self as Resolver>::Choice>>

pub(crate) fn resolve_range( &mut self, args: ArgRange, context: &mut ResolveContext<'_>, ) -> Option<Resolved<<Self as Resolver>::Choice>>

Trait Implementations

impl Clone for ArithmeticResolver

fn clone(&self) -> ArithmeticResolver

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Resolver for ArithmeticResolver

type Choice = (Var, DynIter<dyn Iterator<Item = i64>>)

fn resolve( &mut self, _goal_id: TermId, AppTerm: AppTerm, context: &mut ResolveContext<'_>, ) -> Option<Resolved<Self::Choice>>

fn resume( &mut self, choice: &mut Self::Choice, _goal_id: TermId, context: &mut ResolveContext<'_>, ) -> bool