I want to linearize c=ab using automatic theorem proving. Everything works fine when solving with SMT, but the same way of writing doesn't work for dReal.
`from dreal import
a = Variable('a',Variable.Int)
b = Variable('b',Variable.Int)
c = Variable('c',Variable.Int)
X = [[Variable("x%s%s" %(i+1,j+1), Variable.Int) for j in range(4)] for i in range(4)]
f_sat =forall([a,b,c],
And(
Implies(And(a>=0,a<=1,b>=0,b<=1,c>=0,c<=1,c==ab),And(
X[0][0]a+X[0][1]b+X[0][2]c+X[0][3]<=0,
X[1][0]a+X[1][1]b+X[1][2]c+X[1][3]<=0,
X[2][0]a+X[2][1]b+X[2][2]c+X[2][3]<=0,
X[3][0]a+X[3][1]b+X[3][2]c+X[3][3]<=0,
)),
Implies(And(a>=0,a<=1,b>=0,b<=1,c>=0,c<=1,
X[0][0]a+X[0][1]b+X[0][2]c+X[0][3]<=0,
X[1][0]a+X[1][1]b+X[1][2]c+X[1][3]<=0,
X[2][0]a+X[2][1]b+X[2][2]c+X[2][3]<=0,
X[3][0]a+X[3][1]b+X[3][2]c+X[3][3]<=0,
),c==a*b)
))
result = CheckSatisfiability(f_sat, 0.001)
print(result)`
I want to linearize c=ab using automatic theorem proving. Everything works fine when solving with SMT, but the same way of writing doesn't work for dReal.
`from dreal import a = Variable('a',Variable.Int) b = Variable('b',Variable.Int) c = Variable('c',Variable.Int) X = [[Variable("x%s%s" %(i+1,j+1), Variable.Int) for j in range(4)] for i in range(4)] f_sat =forall([a,b,c], And( Implies(And(a>=0,a<=1,b>=0,b<=1,c>=0,c<=1,c==ab),And( X[0][0]a+X[0][1]b+X[0][2]c+X[0][3]<=0, X[1][0]a+X[1][1]b+X[1][2]c+X[1][3]<=0, X[2][0]a+X[2][1]b+X[2][2]c+X[2][3]<=0, X[3][0]a+X[3][1]b+X[3][2]c+X[3][3]<=0, )), Implies(And(a>=0,a<=1,b>=0,b<=1,c>=0,c<=1, X[0][0]a+X[0][1]b+X[0][2]c+X[0][3]<=0, X[1][0]a+X[1][1]b+X[1][2]c+X[1][3]<=0, X[2][0]a+X[2][1]b+X[2][2]c+X[2][3]<=0, X[3][0]a+X[3][1]b+X[3][2]c+X[3][3]<=0, ),c==a*b) ))
result = CheckSatisfiability(f_sat, 0.001) print(result)`