Skip to content

Commit

Permalink
Merge pull request #388 from pysmt/mathsat-qe-lia
Browse files Browse the repository at this point in the history 
Adding LIA support to MSat-Based Quantifier Elimination
  • Loading branch information
Marco Gario committed Nov 17, 2016
2 parents 1bc0ca2 + 9758a9d commit 1aa86c6
Show file tree
Hide file tree
Showing 6 changed files with 74 additions and 48 deletions.
6 changes: 2 additions & 4 deletions README.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ customize its behavior.
dependencies for building the solver (e.g., make or gcc) and has been
tested mainly on Linux Debian/Ubuntu systems. We suggest that you
refer to the documentation of each solver to understand how to install
it with its python bindings.
it with its python bindings.

For Yices, picosat, and CUDD, we use external wrappers:

Expand Down Expand Up @@ -198,7 +198,7 @@ each of the available quantifier eliminators
Quantifier Eliminator pySMT name Supported Logics
===================== ========== ================
MathSAT FM msat-fm LRA
MathSAT LW msat-lw LRA
MathSAT LW msat-lw LRA, LIA
Z3 z3 LRA, LIA
BDD (CUDD) bdd BOOL
===================== ========== ================
Expand All @@ -221,5 +221,3 @@ pySMT is release under the APACHE 2.0 License.

For further questions, feel free to open an issue, or write to
pysmt@googlegroups.com (`Browse the Archive <https://groups.google.com/d/forum/pysmt>`_).


2 changes: 1 addition & 1 deletion pysmt/factory.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@

DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'btor',
'picosat', 'bdd']
DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_fm', 'msat_lw', 'bdd', 'shannon']
DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_lw', 'msat_fm', 'bdd', 'shannon']
DEFAULT_INTERPOLATION_PREFERENCE_LIST = ['msat', 'z3']
DEFAULT_LOGIC = QF_UFLIRA
DEFAULT_QE_LOGIC = LRA
Expand Down
64 changes: 44 additions & 20 deletions pysmt/solvers/msat.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
except ImportError:
raise SolverAPINotFound

from pysmt.logics import LRA, QF_UFLIA, QF_UFLRA, QF_BV, PYSMT_QF_LOGICS
from pysmt.logics import LRA, LIA, QF_UFLIA, QF_UFLRA, QF_BV, PYSMT_QF_LOGICS
from pysmt.oracles import get_logic

import pysmt.operators as op
Expand All @@ -39,7 +39,8 @@
SolverNotConfiguredForUnsatCoresError,
SolverStatusError,
InternalSolverError,
NonLinearError, PysmtValueError, PysmtTypeError)
NonLinearError, PysmtValueError, PysmtTypeError,
ConvertExpressionError)
from pysmt.decorators import clear_pending_pop, catch_conversion_error
from pysmt.solvers.qelim import QuantifierEliminator
from pysmt.solvers.interpolation import Interpolator
Expand Down Expand Up @@ -524,8 +525,8 @@ def _get_signature(self, term, args):
try:
return self.term_sig[tag](term, args)
except KeyError:
raise PysmtTypeError("Unsupported expression:",
mathsat.msat_term_repr(term))
raise ConvertExpressionError("Unsupported expression:",
mathsat.msat_term_repr(term))

def _sig_binary(self, term, args):
t = self.env.stc.get_type(args[0])
Expand Down Expand Up @@ -605,8 +606,8 @@ def _sig_unknown(self, term, args):
d = mathsat.msat_term_get_decl(term)
fun = self.get_symbol_from_declaration(d)
return fun.symbol_type()
raise PysmtTypeError("Unsupported expression:",
mathsat.msat_term_repr(term))
raise ConvertExpressionError("Unsupported expression:",
mathsat.msat_term_repr(term))

def _back_single_term(self, term, mgr, args):
"""Builds the pysmt formula given a term and the list of formulae
Expand All @@ -633,8 +634,8 @@ def _back_single_term(self, term, mgr, args):
try:
return self.back_fun[tag](term, args)
except KeyError:
raise PysmtTypeError("Unsupported expression:",
mathsat.msat_term_repr(term))
raise ConvertExpressionError("Unsupported expression:",
mathsat.msat_term_repr(term))

def _back_adapter(self, op):
"""Create a function that for the given op.
Expand Down Expand Up @@ -717,8 +718,8 @@ def _back_tag_unknown(self, term, args):
fun = self.get_symbol_from_declaration(d)
res = self.mgr.Function(fun, args)
else:
raise PysmtTypeError("Unsupported expression:",
mathsat.msat_term_repr(term))
raise ConvertExpressionError("Unsupported expression:",
mathsat.msat_term_repr(term))
return res

def get_symbol_from_declaration(self, decl):
Expand Down Expand Up @@ -1082,16 +1083,21 @@ def declare_variable(self, var):
if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
class MSatQuantifierEliminator(QuantifierEliminator, IdentityDagWalker):

LOGICS = [LRA]
LOGICS = [LRA, LIA]

def __init__(self, environment, logic=None, algorithm='fm'):
def __init__(self, environment, logic=None, algorithm='lw'):
"""Initialize the Quantifier Eliminator using 'fm' or 'lw'.
fm: Fourier-Motzkin (default)
lw: Loos-Weisspfenning
"""
if algorithm not in ['fm', 'lw']:
raise PysmtValueError("Algorithm can be either 'fm' or 'lw'")

if logic is not None and (not logic <= LRA and algorithm != "lw"):
raise PysmtValueError("MathSAT quantifier elimination for LIA"\
" only works with 'lw' algorithm")

QuantifierEliminator.__init__(self)
IdentityDagWalker.__init__(self, env=environment)
self.msat_config = mathsat.msat_create_default_config("QF_LRA")
Expand All @@ -1101,19 +1107,26 @@ def __init__(self, environment, logic=None, algorithm='fm'):
self.set_function(self.walk_identity, op.SYMBOL, op.REAL_CONSTANT,
op.BOOL_CONSTANT, op.INT_CONSTANT)
self.logic = logic

self.algorithm = algorithm
self.converter = MSatConverter(environment, self.msat_env)

def eliminate_quantifiers(self, formula):
"""Returns a quantifier-free equivalent formula of `formula`."""
return self.walk(formula)


def exist_elim(self, variables, formula):
logic = get_logic(formula, self.env)
if not logic <= LRA:
raise NotImplementedError("MathSAT quantifier elimination only"\
" supports LRA (detected logic " \
"is: %s)" % str(logic))
if not (logic <= LRA or logic <= LIA):
raise PysmtValueError("MathSAT quantifier elimination only"\
" supports LRA or LIA (detected logic " \
"is: %s)" % str(logic))

if not logic <= LRA and self.algorithm != "lw":
raise PysmtValueError("MathSAT quantifier elimination for LIA"\
" only works with 'lw' algorithm")


fterm = self.converter.convert(formula)
tvars = [self.converter.convert(x) for x in variables]
Expand All @@ -1124,7 +1137,18 @@ def exist_elim(self, variables, formula):

res = mathsat.msat_exist_elim(self.msat_env(), fterm, tvars, algo)

return self.converter.back(res)
try:
return self.converter.back(res)
except ConvertExpressionError:
if logic <= LRA:
raise
raise ConvertExpressionError(message=("Unable to represent" \
"expression %s in pySMT: the quantifier elimination for " \
"LIA is incomplete as it requires the modulus. You can " \
"find the MathSAT term representing the quantifier " \
"elimination as the attribute 'expression' of this " \
"exception object" % str(res)), expression=res)


def walk_forall(self, formula, args, **kwargs):
assert formula.is_forall()
Expand Down Expand Up @@ -1174,9 +1198,9 @@ def _check_logic(self, formulas):
logic = get_logic(f, self.environment)
ok = any(logic <= l for l in self.LOGICS)
if not ok:
raise NotImplementedError(
"Logic not supported by MathSAT interpolation."
"(detected logic is: %s)" % str(logic))
raise PysmtValueError("Logic not supported by MathSAT "
"interpolation. (detected logic is: %s)" \
% str(logic))

def binary_interpolant(self, a, b):
res = self.sequence_interpolant([a, b])
Expand Down
11 changes: 5 additions & 6 deletions pysmt/solvers/z3.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -881,9 +881,9 @@ def __init__(self, environment, logic=None):
def eliminate_quantifiers(self, formula):
logic = get_logic(formula, self.environment)
if not logic <= LRA and not logic <= LIA:
raise NotImplementedError("Z3 quantifier elimination only "\
"supports LRA or LIA without combination."\
"(detected logic is: %s)" % str(logic))
raise PysmtValueError("Z3 quantifier elimination only "\
"supports LRA or LIA without combination."\
"(detected logic is: %s)" % str(logic))

simplifier = z3.Tactic('simplify')
eliminator = z3.Tactic('qe')
Expand Down Expand Up @@ -929,9 +929,8 @@ def _check_logic(self, formulas):
logic = get_logic(f, self.environment)
ok = any(logic <= l for l in self.LOGICS)
if not ok:
raise NotImplementedError(
"Logic not supported by Z3 interpolation."
"(detected logic is: %s)" % str(logic))
raise PysmtValueError("Logic not supported by Z3 interpolation."
"(detected logic is: %s)" % str(logic))

def binary_interpolant(self, a, b):
self._check_logic([a, b])
Expand Down
36 changes: 20 additions & 16 deletions pysmt/test/test_qe.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,15 @@
#
from pysmt.shortcuts import Symbol, ForAll, Exists, And, Iff, GE, LT, Real, Int
from pysmt.shortcuts import Minus, Equals, Plus, ToReal, Implies, LE, TRUE, Not
from pysmt.shortcuts import QuantifierEliminator
from pysmt.shortcuts import Times, QuantifierEliminator
from pysmt.shortcuts import is_sat, is_valid
from pysmt.typing import REAL, BOOL, INT
from pysmt.test import TestCase, main
from pysmt.test import (skipIfNoSolverForLogic, skipIfNoQEForLogic,
skipIfQENotAvailable)
from pysmt.test.examples import get_example_formulae
from pysmt.exceptions import (SolverReturnedUnknownResultError,
NoSolverAvailableError)
from pysmt.exceptions import (SolverReturnedUnknownResultError, PysmtValueError,
NoSolverAvailableError, ConvertExpressionError)
from pysmt.logics import LRA, LIA, UFLIRA


Expand Down Expand Up @@ -61,9 +61,6 @@ def test_selection(self):
with self.assertRaises(NoSolverAvailableError):
QuantifierEliminator(name="nonexistent")

# MathSAT QE does not support LIA
with self.assertRaises(NoSolverAvailableError):
QuantifierEliminator(name="msat", logic=LIA)

@skipIfNoQEForLogic(LRA)
def test_selection_lra(self):
Expand All @@ -80,13 +77,15 @@ def test_qe_z3(self):
self._alternation_int_example(qe)
self._std_examples(qe, LRA)
self._std_examples(qe, LIA)
self._modular_congruence(qe)

# Additional test for raising error on back conversion of
# quantified formulae
p, q = Symbol("p", INT), Symbol("q", INT)

f = ForAll([p], Exists([q], Equals(ToReal(p),
Plus(ToReal(q), ToReal(Int(1))))))
with self.assertRaises(NotImplementedError):
with self.assertRaises(PysmtValueError):
qe.eliminate_quantifiers(f).simplify()


Expand All @@ -99,10 +98,10 @@ def test_qe_msat_fm(self):
self._alternation_real_example(qe)
self._std_examples(qe, LRA)

with self.assertRaises(NotImplementedError):
with self.assertRaises(PysmtValueError):
self._int_example(qe)

with self.assertRaises(NotImplementedError):
with self.assertRaises(PysmtValueError):
self._alternation_int_example(qe)

# Additional test for raising error on back conversion of
Expand All @@ -111,7 +110,7 @@ def test_qe_msat_fm(self):

f = ForAll([p], Exists([q], Equals(ToReal(p),
Plus(ToReal(q), ToReal(Int(1))))))
with self.assertRaises(NotImplementedError):
with self.assertRaises(PysmtValueError):
qe.eliminate_quantifiers(f).simplify()


Expand All @@ -122,22 +121,27 @@ def test_qe_msat_lw(self):
self._real_example(qe)
self._alternation_bool_example(qe)
self._alternation_real_example(qe)
self._int_example(qe)
self._alternation_int_example(qe)
self._std_examples(qe, LIA)

with self.assertRaises(NotImplementedError):
self._int_example(qe)

with self.assertRaises(NotImplementedError):
self._alternation_int_example(qe)
self._modular_congruence(qe)

# Additional test for raising error on back conversion of
# quantified formulae
p, q = Symbol("p", INT), Symbol("q", INT)

f = ForAll([p], Exists([q], Equals(ToReal(p),
Plus(ToReal(q), ToReal(Int(1))))))
with self.assertRaises(NotImplementedError):
with self.assertRaises(PysmtValueError):
qe.eliminate_quantifiers(f).simplify()

def _modular_congruence(self, qe):
p, q = (Symbol(n, INT) for n in "pq")
f = Exists([q], Equals(Times(q, Int(2)), p))
with self.assertRaises(ConvertExpressionError):
qe.eliminate_quantifiers(f)


def _bool_example(self, qe):
# Bool Example
Expand Down
3 changes: 2 additions & 1 deletion pysmt/test/test_regressions.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,8 @@ def test_lia_qe_requiring_modulus(self):
qelim(f)
except ConvertExpressionError as ex:
# The modulus operator must be there
self.assertIn("%2", str(ex.expression))
self.assertTrue("%2" in str(ex.expression) or \
"int_mod_congr" in str(ex.expression))

@skipIfSolverNotAvailable("msat")
def test_msat_partial_model(self):
Expand Down

0 comments on commit 1aa86c6

Please sign in to comment.