How to solve both real and integer problems simultaneously？

[jian cao]

 I encountered a problem and found that variables can only be solved simultaneously as integers or real numbers。

from pysmt.shortcuts import *
from pysmt.typing import *

hello = [Symbol(s, INT) for s in "hello"]
pysmt = [Symbol(s, REAL) for s in "pysmt"]
domains_1 = And([And(GE(l, Int(1)),
                   LT(l, Int(10))) for l in hello])
domains_2 = And([And(GE(l, Real(1)),
                   LT(l, Real(10))) for l in pysmt])

hello = [Symbol(s, INT) for s in "hello"]
pysmt = [Symbol(s, REAL) for s in "pysmt"]
domains_1 = And([And(GE(l, Int(1)),
                   LT(l, Int(10))) for l in hello])
domains_2 = And([And(GE(l, Real(1)),
                   LT(l, Real(10))) for l in pysmt])

sum_hello = Plus(hello) # n-ary operators can take lists
sum_pysmt = Plus(pysmt) # as arguments
problem = And(Equals(sum_hello, sum_pysmt),
              Equals(sum_hello, Int(25)))
formula = And(domains_1, domains_2, problem)

print("Serialization of the formula:")
print(formula)

model = get_model(formula, solver_name="z3")
if model:
  print(model)
else:
  print("No solution found")

--------------------------------------------------------------------------- PysmtTypeError Traceback (most recent call last) Input In [2], in <cell line: 10>() 8 sum_hello = Plus(hello) # n-ary operators can take lists 9 sum_pysmt = Plus(pysmt) # as arguments ---> 10 problem = And(Equals(sum_hello, sum_pysmt), 11 Equals(sum_hello, Int(25))) 12 formula = And(domains_1, domains_2, problem) 14 print("Serialization of the formula:") File D:\python38\lib\site-packages\pysmt\shortcuts.py:209, in Equals(left, right) 207 def Equals(left, right): 208 r""".. math:: l = r""" --> 209 return get_env().formula_manager.Equals(left, right) File D:\python38\lib\site-packages\pysmt\formula.py:284, in FormulaManager.Equals(self, left, right) 279 def Equals(self, left, right): 280 """ Creates an expression of the form: left = right 281 282 For the boolean case use Iff 283 """ --> 284 return self.create_node(node_type=op.EQUALS, 285 args=(left, right)) File D:\python38\lib\site-packages\pysmt\formula.py:96, in FormulaManager.create_node(self, node_type, args, payload) 94 self._next_free_id += 1 95 self.formulae[content] = n ---> 96 self._do_type_check(n) 97 return n File D:\python38\lib\site-packages\pysmt\formula.py:81, in FormulaManager._do_type_check_real(self, formula) 80 def _do_type_check_real(self, formula): ---> 81 self.get_type(formula) File D:\python38\lib\site-packages\pysmt\type_checker.py:45, in SimpleTypeChecker.get_type(self, formula) 43 res = self.walk(formula) 44 if not self.be_nice and res is None: ---> 45 raise PysmtTypeError("The formula '%s' is not well-formed" \ 46 % str(formula)) 47 return res PysmtTypeError: The formula '((h + e + l + l + o) = (p + y + s + m + t))' is not well-formed

[Andrea Micheli]

Hello Jian,

sorry for the late reply.

Pysmt is strict about typing, you cannot compare an integaer and a real (nor you can use an integer where a real is expected).

A much simpler example of this behavior is:

f = Equals(Int(1), Real(1))

This is not allowed in pysmt, as we are not doing automatic promotion of INT to REAL. The solution is to use the ToReal() operator to explicitly cast Integers into Reals:

f = Equals(ToReal(Int(1)), Real(1))

A final note: when you encode your problem you should think carefully if you really need a mixture of real and integer variables or not, because mixing them makes the problem jum in the QF_LIRA logic which can be harder to solve than QF_LRA (that is when you only use reals).

HTH

Andrea

 

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/dbb982ef-ca9f-4bc5-9f00-0cdedfd6498an%40googlegroups.com.

--

Le informazioni contenute nella presente comunicazione sono di natura privata e come tali sono da considerarsi riservate ed indirizzate esclusivamente ai destinatari indicati e per le finalità strettamente legate al relativo contenuto. Se avete ricevuto questo messaggio per errore, vi preghiamo di eliminarlo e di inviare una comunicazione all’indirizzo e-mail del mittente.

--

The information transmitted is intended only for the person or entity to which it is addressed and may contain confidential and/or privileged material. If you received this in error, please contact the sender and delete the material.