Uses of Interface
dev.civl.sarl.IF.expr.BooleanExpression
Packages that use BooleanExpression
Package
Description
This package provides the internal interface for the representation of basic
symbolic expressions.
The ideal module supports reasoning about numerical expressions using "ideal"
mathematical reals and integers.
This package and its subpackages provide the "public interface" to SARL.
The public interface package dealing with symbolic expressions.
Module "prove" constitutes the interface between SARL and (possibly external)
theorem provers.
The internal interface for the "reason" module, which deals with
Reasoners --- objects used to prove
theorems and simplify symbolic expressions.Interfaces for the simplification of symbolic expressions.
-
Uses of BooleanExpression in dev.civl.sarl.expr.IF
Methods in dev.civl.sarl.expr.IF that return BooleanExpressionModifier and TypeMethodDescriptionBooleanExpressionFactory.and(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the conjunction of the two given arguments.BooleanExpressionFactory.booleanExpression(SymbolicExpression.SymbolicOperator operator, SymbolicObject... args) Returns an expression, given the operator and an array of argumentsSymbolicRangeFactory.disjoint(SymbolicRange range0, SymbolicRange range1) NOTE: Currently only support ranges with a step value of 1.NumericExpressionFactory.equals(NumericExpression arg0, NumericExpression arg1) Returns a BooleanExpression with the result of the equals operation on 2 NumericExpressionsSymbolicRangeFactory.equals(SymbolicRange range0, SymbolicRange range1) NOTE: Currently only support ranges with a step value of 1.BooleanExpressionFactory.exists(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the existentially quantified expression exists(x).e.BooleanExpressionFactory.factorOrs(BooleanExpression[] orExpressions) Given an array of or-expressions (expressions with operationSymbolicExpression.SymbolicOperator.OR), this method computes the "greatest common divisor" of those expressions and replaces each element of the array with the expressions that results from "dividing by" that gcd.BooleanExpressionFactory.falseExpr()Returns a false BooleanExpressionBooleanExpressionFactory.forall(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the universally quantified expression forall(x).e.BooleanExpressionFactory.getArgumentsAsArray(BooleanExpression expression) Given aBooleanExpressionwith operatorSymbolicExpression.SymbolicOperator.AND,SymbolicExpression.SymbolicOperator.OR, orSymbolicExpression.SymbolicOperator.NOT, this method returns the arguments of that operator as an array.SymbolicRangeFactory.inRange(NumericExpression expr, SymbolicRange range) NumericExpressionFactory.lessThan(NumericExpression arg0, NumericExpression arg1) Returns a BooleanExpression with the result of the lessThan operation on 2 NumericExpressionsNumericExpressionFactory.lessThanEquals(NumericExpression arg0, NumericExpression arg1) Returns a BooleanExpression with the result of the lessThanEquals operation on 2 NumericExpressionsNumericExpressionFactory.neq(NumericExpression arg0, NumericExpression arg1) Returns a BooleanExpression with the result of the notEquals operation on 2 NumericExpressionsSymbolicRangeFactory.neq(SymbolicRange range0, SymbolicRange range1) NOTE: Currently only support ranges with a step value of 1.BooleanExpressionFactory.not(BooleanExpression arg) Returns a symbolic expression representing the logical negation of the given expression arg.NumericExpressionFactory.notLessThan(NumericExpression arg0, NumericExpression arg1) Returns a BooleanExpression with the result of the notLessThan operation on 2 NumericExpressionsNumericExpressionFactory.notLessThanEquals(NumericExpression arg0, NumericExpression arg1) Returns a BooleanExpression with the result of the notLessThanEquals operation on 2 NumericExpressionsBooleanExpressionFactory.or(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the disjunction of the two given arguments.BooleanExpressionFactory.or(Iterable<? extends BooleanExpression> args) Returns a symbolic expression which represents the disjunction of the expressions in the given array args.SymbolicRangeFactory.strictlyBelow(SymbolicRange range0, SymbolicRange range1) NOTE: Currently only support ranges with a step value of 1.SymbolicRangeFactory.subset(SymbolicRange range0, SymbolicRange range1) NOTE: Currently only support ranges with a step value of 1.BooleanExpressionFactory.symbolic(boolean value) Short cut for symbolic(booleanObject(value)).BooleanExpressionFactory.symbolic(BooleanObject object) The symbolic expression wrapping the given boolean object (true or false).BooleanExpressionFactory.trueExpr()Returns a true BooleanExpressionExpressionFactory.valueSetContains(SymbolicType valueType, SymbolicExpression refArr0, SymbolicExpression refArr1) Test if an array of value set references "refArr0", that is associated with the given "valueType", contains another array of value set references "refArr1", that is associated with the given "valueType" as well.ExpressionFactory.valueSetRefereceNoIntersect(SymbolicType valueType, ValueSetReference ref0, ValueSetReference ref1) Tests if the two givenValueSetReferences have NO intersection, i.e., if applying the two reference to the same object, if their referred parts have no overlap.Methods in dev.civl.sarl.expr.IF that return types with arguments of type BooleanExpressionModifier and TypeMethodDescriptionBooleanExpressionFactory.getBooleanComparator()Returns aComparatoronBooleanExpressions produced by this factory.Methods in dev.civl.sarl.expr.IF with parameters of type BooleanExpressionModifier and TypeMethodDescriptionBooleanExpressionFactory.and(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the conjunction of the two given arguments.booleanBooleanExpressionFactory.containsArgument(BooleanExpression expression, SymbolicObject arg) Is one of the arguments of the given expression equal toarg?BooleanExpressionFactory.exists(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the existentially quantified expression exists(x).e.BooleanExpressionFactory.factorOrs(BooleanExpression[] orExpressions) Given an array of or-expressions (expressions with operationSymbolicExpression.SymbolicOperator.OR), this method computes the "greatest common divisor" of those expressions and replaces each element of the array with the expressions that results from "dividing by" that gcd.BooleanExpressionFactory.forall(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the universally quantified expression forall(x).e.BooleanExpressionFactory.getArgumentsAsArray(BooleanExpression expression) Given aBooleanExpressionwith operatorSymbolicExpression.SymbolicOperator.AND,SymbolicExpression.SymbolicOperator.OR, orSymbolicExpression.SymbolicOperator.NOT, this method returns the arguments of that operator as an array.BooleanExpressionFactory.not(BooleanExpression arg) Returns a symbolic expression representing the logical negation of the given expression arg.BooleanExpressionFactory.or(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the disjunction of the two given arguments.Method parameters in dev.civl.sarl.expr.IF with type arguments of type BooleanExpressionModifier and TypeMethodDescriptionBooleanExpressionFactory.or(Iterable<? extends BooleanExpression> args) Returns a symbolic expression which represents the disjunction of the expressions in the given array args. -
Uses of BooleanExpression in dev.civl.sarl.ideal.IF
Methods in dev.civl.sarl.ideal.IF that return BooleanExpressionModifier and TypeMethodDescriptionIdealFactory.isNonnegative(RationalExpression rational) Given a rational expressionrationalreturns an expression equivalent to 0≤rational.Computes an expression equivalent to "monomial != 0".IdealFactory.isPositive(RationalExpression rational) Given a rational expressionrationalreturns an expression equivalent to 0<rational.Computes boolean expression equivalent to m=0. -
Uses of BooleanExpression in dev.civl.sarl.IF
Fields in dev.civl.sarl.IF declared as BooleanExpressionModifier and TypeFieldDescriptionCoreUniverse.ForallStructure.bodyThe body of the expression: the boolean formula that is claimed to hold if i is between the lower and upper bounds (inclusive).Methods in dev.civl.sarl.IF that return BooleanExpressionModifier and TypeMethodDescriptionCoreUniverse.and(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the conjunction of the two given arguments.CoreUniverse.and(Iterable<? extends BooleanExpression> args) Returns a symbolic expression which represents the conjunction of the expressions in the given array args.CoreUniverse.bool(boolean value) Short cut for symbolic(booleanObject(value)).CoreUniverse.bool(BooleanObject object) The symbolic expression wrapping the given boolean object (true or false).CoreUniverse.compatible(SymbolicType type0, SymbolicType type1) Returns a boolean expression which holds iff the two types are compatible.CoreUniverse.differentiable(SymbolicExpression function, IntObject degree, Iterable<? extends NumericExpression> lowerBounds, Iterable<? extends NumericExpression> upperBounds) Returns an expression of boolean type which encodes the claim that a function is differentiable on a closed interval in R^n.CoreUniverse.divides(NumericExpression a, NumericExpression b) Does the integer a divide the integer b evenly? I.e, does there exist an integer n such that b=a*n?CoreUniverse.equals(SymbolicExpression arg0, SymbolicExpression arg1) Returns expression equivalent to arg0 = arg1 ("equals").CoreUniverse.equiv(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing "p is equivalent to q", i.e., pinvalid input: '<'=>q.CoreUniverse.exists(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the existentially quantified expression exists(x).e.CoreUniverse.existsInt(NumericSymbolicConstant index, NumericExpression low, NumericExpression high, BooleanExpression predicate) A special case of "exists" that is very common: exists integer i such that lowinvalid input: '<'=iinvalid input: '<'high and p(i).CoreUniverse.falseExpression()Returns the boolean literal false.CoreUniverse.forall(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the universally quantified expression forall(x).e.CoreUniverse.forallInt(NumericSymbolicConstant index, NumericExpression low, NumericExpression high, BooleanExpression predicate) A special case of "forall" that is very common: forall integers i such that lowinvalid input: '<'=iinvalid input: '<'high, p(i).Reasoner.getFullCollapsedContext()Returns the full context associated to this Reasoner.Reasoner.getFullContext(int index) Reasoner.getReducedCollapsedContext()Returns the reduced context associated to this Reasoner.Reasoner.getReducedContext(int index) CoreUniverse.implies(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing "p implies q", i.e., p=>q.CoreUniverse.isSubsetOf(SymbolicExpression set1, SymbolicExpression set2) CoreUniverse.lessThan(NumericExpression arg0, NumericExpression arg1) Returns expression equivalent to arg0 invalid input: '<' arg1.CoreUniverse.lessThanEquals(NumericExpression arg0, NumericExpression arg1) Returns expression equivalent to arg0 invalid input: '<'= arg1 ("less than or equal to").CoreUniverse.neq(SymbolicExpression arg0, SymbolicExpression arg1) Returns expression equivalent to arg0 != arg1 ("not equals").CoreUniverse.not(BooleanExpression arg) Returns a symbolic expression representing the logical negation of the given expression arg.CoreUniverse.or(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the disjunction of the two given arguments.CoreUniverse.or(Iterable<? extends BooleanExpression> args) Returns a symbolic expression which represents the disjunction of the expressions in the given array args.CoreUniverse.permut(SymbolicExpression array_a, SymbolicExpression array_b, NumericExpression low, NumericExpression high) A permutation predicate, which asserts the slice from lower indexlowto higher indexhighin arrayarray_ais a permutation of the slice from lower indexlowto higher indexhighin arrayarray_b.CoreUniverse.quickEquals(SymbolicExpression arg0, SymbolicExpression arg1) CoreUniverse.removeQuantifiers(BooleanExpression arg) Returns arg with all clauses containing quantifers removed.CoreUniverse.trueExpression()Returns the boolean literal true.CoreUniverse.unionTest(IntObject memberIndex, SymbolicExpression object) Tests whether an object of a union type is in the image of injection from the member type of the given index.CoreUniverse.valueSetContains(SymbolicExpression vst0, SymbolicExpression vst1) Test if a value set templatevst0contains another value set templatevst1.CoreUniverse.valueSetNoIntersect(SymbolicExpression vst0, SymbolicExpression vst1) Test if two value set templates have no intersection, i.e., if applying the two templates to the same object, their referred parts have no overlap.Methods in dev.civl.sarl.IF that return types with arguments of type BooleanExpressionModifier and TypeMethodDescriptionReasoner.getFullContextStack()Reasoner.getReducedContextStack()Methods in dev.civl.sarl.IF with parameters of type BooleanExpressionModifier and TypeMethodDescriptionCoreUniverse.and(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the conjunction of the two given arguments.booleanReasoner.checkBigOClaim(BooleanExpression constraint, NumericExpression lhs, NumericSymbolicConstant[] limitVars, int[] orders) Attempts to prove a uniform "Big-O" claim.CoreUniverse.cond(BooleanExpression predicate, SymbolicExpression trueCase, SymbolicExpression falseCase) "If-then-else" expression.CoreUniverse.equiv(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing "p is equivalent to q", i.e., pinvalid input: '<'=>q.CoreUniverse.exists(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the existentially quantified expression exists(x).e.CoreUniverse.existsInt(NumericSymbolicConstant index, NumericExpression low, NumericExpression high, BooleanExpression predicate) A special case of "exists" that is very common: exists integer i such that lowinvalid input: '<'=iinvalid input: '<'high and p(i).CoreUniverse.extractBoolean(BooleanExpression expression) If the given expression has a concreteBooleanvalue, this returns it, else it returnsnull.SymbolicUniverse.extractNumber(BooleanExpression assumption, NumericExpression expression) Attempts to extract a concrete numeric value from the given expression, using the assumption if necessary to simplify the expression.CoreUniverse.forall(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the universally quantified expression forall(x).e.CoreUniverse.forallInt(NumericSymbolicConstant index, NumericExpression low, NumericExpression high, BooleanExpression predicate) A special case of "forall" that is very common: forall integers i such that lowinvalid input: '<'=iinvalid input: '<'high, p(i).CoreUniverse.getForallStructure(BooleanExpression forallExpr) Attempts to find a boolean expression equivalent toforallExprbut with the structureCoreUniverse.implies(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing "p implies q", i.e., p=>q.booleanReasoner.isValid(BooleanExpression predicate) Equivalent tovalid(predicate).getResultType()==ResultType.YES.CoreUniverse.not(BooleanExpression arg) Returns a symbolic expression representing the logical negation of the given expression arg.CoreUniverse.or(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the disjunction of the two given arguments.SymbolicUniverse.reasoner(BooleanExpression context) Returns aReasonerfor the given context.CoreUniverse.removeQuantifiers(BooleanExpression arg) Returns arg with all clauses containing quantifers removed.Reasoner.unsat(BooleanExpression predicate) Attempts to determine whether the statement p(x) invalid input: '&'invalid input: '&' q(x) is unsatisfiable.Reasoner.valid(BooleanExpression predicate) Attempts to determine whether the statement p(x)=>q(x) is a tautology.Reasoner.validOrModel(BooleanExpression predicate) Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counter-example).SymbolicUniverse.valueSetElimWidening(BooleanExpression context, SymbolicExpression vst, SymbolicExpression elimExpr, SymbolicExpression lower, SymbolicExpression upper) SymbolicUniverse.valueSetProtectiveWidening(BooleanExpression context, SymbolicExpression vstM, SymbolicExpression vstP) SymbolicUniverse.valueSetWidening(BooleanExpression context, SymbolicExpression vst) Apply a default widening operator to the value set references in the given value set template.Method parameters in dev.civl.sarl.IF with type arguments of type BooleanExpressionModifier and TypeMethodDescriptionCoreUniverse.and(Iterable<? extends BooleanExpression> args) Returns a symbolic expression which represents the conjunction of the expressions in the given array args.CoreUniverse.or(Iterable<? extends BooleanExpression> args) Returns a symbolic expression which represents the disjunction of the expressions in the given array args.SymbolicUniverse.reasoner(List<BooleanExpression> contextStack) CoreUniverse.reduction(SymbolicExpression[] operands, NumericExpression count, SymbolicExpression op, List<BooleanExpression> compatibleConditionsOutput) a$reductionfunction that takes a list of operands, the number of elements per operand and an operator, returns the element-wise reduction result of the operator over the operands. -
Uses of BooleanExpression in dev.civl.sarl.IF.expr
Subinterfaces of BooleanExpression in dev.civl.sarl.IF.exprMethods in dev.civl.sarl.IF.expr that return BooleanExpressionModifier and TypeMethodDescriptionBooleanExpression.getClauses()Returns a sequence of boolean expressions whose conjunction is equivalent tothis. -
Uses of BooleanExpression in dev.civl.sarl.prove.IF
Methods in dev.civl.sarl.prove.IF with parameters of type BooleanExpressionModifier and TypeMethodDescriptionTheoremProverFactory.newProver(BooleanExpression context) Returns a new instance ofTheoremProverwith the given context.TheoremProverFactory.newProver(BooleanExpression context, ProverFunctionInterpretation[] logicFunctions) Returns a new instance ofTheoremProverwith the given context.TheoremProver.unsat(BooleanExpression predicate) Attempts to determine whether the statement p(x) invalid input: '&'invalid input: '&' q(x) is unsatisfiable.TheoremProver.valid(BooleanExpression predicate) Attempts to determine whether the statement p(x)=>q(x) is valid, i.e., is a tautology.TheoremProver.validOrModel(BooleanExpression predicate) Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counterexample). -
Uses of BooleanExpression in dev.civl.sarl.reason.IF
Methods in dev.civl.sarl.reason.IF with parameters of type BooleanExpressionModifier and TypeMethodDescriptionReasonerFactory.getReasoner(BooleanExpression context, boolean useBackwardSubstitution, ProverFunctionInterpretation[] proverPredicates) Gets aReasonerfor the givencontext.Method parameters in dev.civl.sarl.reason.IF with type arguments of type BooleanExpressionModifier and TypeMethodDescriptionReasonerFactory.getReasoner(List<BooleanExpression> contextStack, boolean useBackwardSubstitution, ProverFunctionInterpretation[] proverPredicates) -
Uses of BooleanExpression in dev.civl.sarl.simplify.IF
Methods in dev.civl.sarl.simplify.IF that return BooleanExpressionModifier and TypeMethodDescriptionRange.symbolicRepresentation(NumericExpression x, PreUniverse universe) Methods in dev.civl.sarl.simplify.IF that return types with arguments of type BooleanExpressionModifier and TypeMethodDescriptionContextPartition.minimizeFor(SymbolicExpression expr, PreUniverse universe) Returns a formula equivalent to or weaker than the original context but which can be used as the context for check validity or simplifyingexpr.Method parameters in dev.civl.sarl.simplify.IF with type arguments of type BooleanExpressionModifier and TypeMethodDescriptionstatic ContextPartitionSimplify.newContextPartition(PreUniverse universe, List<BooleanExpression> contextStack)