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)
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 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 85 of file UserPropagatorBase.java.

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

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

conflict() [1/2]

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

inline

Definition at line 89 of file UserPropagatorBase.java.

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

conflict() [2/2]

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

inline

Definition at line 93 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 97 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 75 of file UserPropagatorBase.java.

{}

Referenced by UserPropagateBase.add_created(), and UserPropagatorBase.createdWrapper().

createdWrapper()

final void createdWrapper ( long  last )

inlineprotected

Definition at line 52 of file UserPropagatorBase.java.

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

decide()

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

inline

Definition at line 81 of file UserPropagatorBase.java.

{}

Referenced by UserPropagateBase.add_decide(), and UserPropagatorBase.decideWrapper().

decideWrapper()

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

inlineprotected

Definition at line 64 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 79 of file UserPropagatorBase.java.

{}

Referenced by AstRef.__eq__(), UserPropagateBase.add_eq(), SortRef.cast(), BoolSortRef.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 83 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 77 of file UserPropagatorBase.java.

{}

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

fixedWrapper()

final void fixedWrapper ( long  lvar, long  lvalue  )

inlineprotected

Definition at line 57 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 47 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 103 of file UserPropagatorBase.java.

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

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();
    }