Open
Description
I'm unable to properly handle formulas that have uninterpreted functions and nonlinear reals.
I know that SMT2 lib only has AUFNIRA but both z3 and cvc5 should be able to handle such inputs but I'm unable to make it work properly in pysmt. See below
from pysmt.shortcuts import Symbol, ForAll, is_sat
from pysmt.typing import REAL
from pysmt import logics
x = Symbol("x", REAL)
y = Symbol("y", REAL)
f = ForAll([x,y], x * y < 3 * x)
print(is_sat(f, solver_name='z3',logic=logics.UFLRA)) # prints False (correctly, even though this is not linear)
print(is_sat(f, solver_name='cvc5',logic=logics.UFLRA)) # runtime error in cvc5
print(is_sat(f, solver_name='z3',logic=logics.AUFNIRA)) # pysmt.exceptions.NoSolverAvailableError: Solver 'z3' does not support logic AUFNIRA
print(is_sat(f)) # pysmt.exceptions.NoLogicAvailableError: Logic Detected Logic is not supported
Metadata
Metadata
Assignees
Labels
No labels