UserPropagatorBase Class Reference

Inheritance diagram for UserPropagatorBase:

Public Member Functions
	UserPropagatorBase (Context _ctx, Solver _solver)
final Context	getCtx ()
final Solver	getSolver ()
abstract void	push ()
abstract void	pop (int number)
abstract UserPropagatorBase	fresh (Context ctx)
void	created (Expr<?> ast)
void	fixed (Expr<?> var, Expr<?> value)
void	eq (Expr<?> x, Expr<?> y)
boolean	on_binding (Expr<?> q, Expr<?> inst)
void	decide (Expr<?> var, int bit, boolean is_pos)
void	fin ()
final void	add (Expr<?> expr)
final boolean	conflict (Expr<?>[] fixed)
final boolean	conflict (Expr<?>[] fixed, Expr<?>[] lhs, Expr<?>[] rhs)
final boolean	consequence (Expr<?>[] fixed, Expr<?>[] lhs, Expr<?>[] rhs, Expr<?> conseq)
final boolean	nextSplit (Expr<?> e, long idx, Z3_lbool phase)

Protected Member Functions
final void	pushWrapper ()
final void	popWrapper (int number)
final void	finWrapper ()
final void	eqWrapper (long lx, long ly)
final boolean	onBindingWrapper (long lq, long linst)
final UserPropagatorBase	freshWrapper (long lctx)
final void	createdWrapper (long last)
final void	fixedWrapper (long lvar, long lvalue)
final void	decideWrapper (long lvar, int bit, boolean is_pos)

Detailed Description

Definition at line 6 of file UserPropagatorBase.java.

Constructor & Destructor Documentation

UserPropagatorBase()

UserPropagatorBase ( Context  _ctx, Solver  _solver  )

inline

Definition at line 10 of file UserPropagatorBase.java.

                                                            {
        super(_ctx.nCtx(), _solver.getNativeObject());   
        ctx = _ctx;
        solver = _solver; 
    }

Member Function Documentation

add()

final void add ( Expr<?>  expr )

inline

Definition at line 94 of file UserPropagatorBase.java.

                                        {
        Native.propagateAdd(this, ctx.nCtx(), solver.getNativeObject(), javainfo, expr.getNativeObject());
    }

Referenced by Solver.__iadd__().

conflict() [1/2]

final boolean conflict ( Expr<?>[]  fixed )

inline

Definition at line 98 of file UserPropagatorBase.java.

                                                   {
        return conflict(fixed, new Expr[0], new Expr[0]);
    }

Referenced by UserPropagatorBase.conflict().

conflict() [2/2]

final boolean conflict ( Expr<?>[]  fixed, Expr<?>[]  lhs, Expr<?>[]  rhs  )

inline

Definition at line 102 of file UserPropagatorBase.java.

                                                                                 {
        return consequence(fixed, lhs, rhs, ctx.mkBool(false));
    }

consequence()

final boolean consequence ( Expr<?>[]  fixed, Expr<?>[]  lhs, Expr<?>[]  rhs, Expr<?>  conseq  )

inline

Definition at line 106 of file UserPropagatorBase.java.

                                                                                                    {
        return Native.propagateConsequence(
            this, ctx.nCtx(), solver.getNativeObject(), javainfo,
            fixed.length, AST.arrayToNative(fixed), lhs.length, AST.arrayToNative(lhs), AST.arrayToNative(rhs), conseq.getNativeObject());
    }

Referenced by UserPropagatorBase.conflict().

created()

void created ( Expr<?>  ast )

inline

Definition at line 82 of file UserPropagatorBase.java.

{}

Referenced by UserPropagatorBase.createdWrapper().

createdWrapper()

final void createdWrapper ( long  last )

inlineprotected

Definition at line 59 of file UserPropagatorBase.java.

                                                   {
        created(new Expr(ctx, last));
    }

decide()

void decide ( Expr<?>  var, int  bit, boolean  is_pos  )

inline

Definition at line 90 of file UserPropagatorBase.java.

{}

Referenced by UserPropagatorBase.decideWrapper().

decideWrapper()

final void decideWrapper ( long  lvar, int  bit, boolean  is_pos  )

inlineprotected

Definition at line 71 of file UserPropagatorBase.java.

                                                                           {
        Expr var = new Expr(ctx, lvar);
        decide(var, bit, is_pos);
    }

eq()

void eq ( Expr<?>  x, Expr<?>  y  )

inline

Definition at line 86 of file UserPropagatorBase.java.

{}

Referenced by AstRef.__eq__(), SortRef.cast(), and UserPropagatorBase.eqWrapper().

eqWrapper()

final void eqWrapper ( long  lx, long  ly  )

inlineprotected

Definition at line 40 of file UserPropagatorBase.java.

                                                     {
        Expr x = new Expr(ctx, lx);
        Expr y = new Expr(ctx, ly);
        eq(x, y);
    }

fin()

void fin ( )

inline

Definition at line 92 of file UserPropagatorBase.java.

{}

Referenced by UserPropagatorBase.finWrapper().

finWrapper()

final void finWrapper ( )

inlineprotected

Definition at line 35 of file UserPropagatorBase.java.

                                      {
        fin();
    }

fixed()

void fixed ( Expr<?>  var, Expr<?>  value  )

inline

Definition at line 84 of file UserPropagatorBase.java.

{}

Referenced by UserPropagatorBase.conflict(), UserPropagatorBase.conflict(), UserPropagatorBase.consequence(), and UserPropagatorBase.fixedWrapper().

fixedWrapper()

final void fixedWrapper ( long  lvar, long  lvalue  )

inlineprotected

Definition at line 64 of file UserPropagatorBase.java.

                                                              {
        Expr var = new Expr(ctx, lvar);
        Expr value = new Expr(ctx, lvalue);
        fixed(var, value);
    }

fresh()

abstract UserPropagatorBase fresh ( Context  ctx )

abstract

Referenced by UserPropagatorBase.freshWrapper().

freshWrapper()

final UserPropagatorBase freshWrapper ( long  lctx )

inlineprotected

Definition at line 54 of file UserPropagatorBase.java.

                                                               {
        return fresh(new Context(lctx));
    }

getCtx()

final Context getCtx ( )

inline

Definition at line 16 of file UserPropagatorBase.java.

                                  {
        return ctx;
    }

getSolver()

final Solver getSolver ( )

inline

Definition at line 20 of file UserPropagatorBase.java.

                                    {
        return solver;
    }

nextSplit()

final boolean nextSplit ( Expr<?>  e, long  idx, Z3_lbool  phase  )

inline

Definition at line 112 of file UserPropagatorBase.java.

                                                                        {
        return Native.propagateNextSplit(
            this, ctx.nCtx(), solver.getNativeObject(), javainfo,
            e.getNativeObject(), idx, phase.toInt());
    }

on_binding()

boolean on_binding ( Expr<?>  q, Expr<?>  inst  )

inline

Definition at line 88 of file UserPropagatorBase.java.

{ return true; }

Referenced by UserPropagatorBase.onBindingWrapper().

onBindingWrapper()

final boolean onBindingWrapper ( long  lq, long  linst  )

inlineprotected

Definition at line 47 of file UserPropagatorBase.java.

                                                                  {
        Expr q = new Expr(ctx, lq);
        Expr inst = new Expr(ctx, linst);
        return on_binding(q, inst);
    }

pop()

abstract void pop ( int  number )

abstract

Referenced by Solver.__exit__(), and UserPropagatorBase.popWrapper().

popWrapper()

final void popWrapper ( int  number )

inlineprotected

Definition at line 30 of file UserPropagatorBase.java.

                                                {
        pop(number);
    }

push()

abstract void push ( )

abstract

Referenced by Solver.__enter__(), and UserPropagatorBase.pushWrapper().

pushWrapper()

final void pushWrapper ( )

inlineprotected

Definition at line 25 of file UserPropagatorBase.java.

                                       {
        push();
    }