Skip to content
Snippets Groups Projects
Commit 3e74fe12 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Support InequalitySplit for Int32

parent c691fe52
No related branches found
No related tags found
No related merge requests found
...@@ -14,7 +14,10 @@ case object InequalitySplit extends Rule("Ineq. Split.") { ...@@ -14,7 +14,10 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = { def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory) val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory)
val candidates = p.as.filter(_.getType == IntegerType).combinations(2).toList.filter { val argsPairs = p.as.filter(_.getType == IntegerType).combinations(2) ++
p.as.filter(_.getType == Int32Type).combinations(2)
val candidates = argsPairs.toList.filter {
case List(a1, a2) => case List(a1, a2) =>
val toValLT = implies(p.pc, LessThan(Variable(a1), Variable(a2))) val toValLT = implies(p.pc, LessThan(Variable(a1), Variable(a2)))
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment