Skip to content

Commit

Permalink
Merge pull request #423 from pysmt/quantified-bv
Browse files Browse the repository at this point in the history 
Add support for BV and UFBV
  • Loading branch information
@mikand
mikand committed Aug 1, 2017
2 parents 01149c3 + 15963df commit b4e6a59
Show file tree
Hide file tree
Showing 8 changed files with 122 additions and 100 deletions.
14 changes: 13 additions & 1 deletion pysmt/logics.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -439,6 +439,18 @@ def __hash__(self):
quantifier_free=True,
bit_vectors=True)

BV = Logic(name="BV",
description=\
"""Closed formulas over the theory of fixed-size
bitvectors.""",
bit_vectors=True)

UFBV = Logic(name="UFBV",
description=\
"""Closed formulas over the theory of fixed-size bitvectors
and uninterpreted functions.""",
bit_vectors=True,
uninterpreted=True)

QF_IDL = Logic(name="QF_IDL",
description=\
Expand Down Expand Up @@ -640,7 +652,7 @@ def __hash__(self):
QF_BV, QF_UFBV,
QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX,
QF_AUFBVLIRA,
QF_NRA, QF_NIA,
QF_NRA, QF_NIA, UFBV, BV,
])

# PySMT Supports constant arrays: We auto-generate these logics
Expand Down
200 changes: 106 additions & 94 deletions pysmt/test/smtlib/parser_utils.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,98 +22,11 @@
from pysmt.shortcuts import get_env, reset_env
from pysmt.smtlib.parser import SmtLibParser, get_formula_fname
from pysmt.smtlib.script import check_sat_filter
from pysmt.logics import QF_LIA, QF_LRA, LRA, QF_UFLIRA, QF_UFBV, QF_BV
from pysmt.logics import QF_ALIA, QF_ABV, QF_AUFLIA, QF_AUFBV, QF_NRA, QF_NIA
from pysmt.logics import (QF_LIA, QF_LRA, LRA, QF_UFLIRA, QF_UFBV, QF_BV,
QF_ALIA, QF_ABV, QF_AUFLIA, QF_AUFBV, QF_NRA, QF_NIA,
UFBV, BV)
from pysmt.exceptions import NoSolverAvailableError, SolverReturnedUnknownResultError

SMTLIB_DIR = "pysmt/test/smtlib"
SMTLIB_TEST_FILES = [
#
# QF_LIA
#
(QF_LIA, "small_set/QF_LIA/prp-23-47.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-20-46.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-24-47.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-24-46.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-22-46.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-25-49.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-21-46.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-23-46.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-25-48.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-25-47.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-24-48.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/prp-25-46.smt2.bz2", "unsat"),
(QF_LIA, "small_set/QF_LIA/issue_159.smt2.bz2", "sat"),
#
# QF_LRA
#
(QF_LRA, "small_set/QF_LRA/uart-8.induction.cvc.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/uart-10.induction.cvc.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/uart-18.induction.cvc.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/uart-26.induction.cvc.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/uart-11.induction.cvc.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/uart-16.induction.cvc.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/uart-6.induction.cvc.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/uart-14.induction.cvc.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_11nodes.abstract.base.smt2.bz2", "unsat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_8nodes.synchro.base.smt2.bz2", "unsat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_3nodes.bug.induct.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_15nodes.abstract.base.smt2.bz2", "unsat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_12nodes.synchro.base.smt2.bz2", "unsat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_8nodes.missing.induct.smt2.bz2", "sat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_14nodes.abstract.base.smt2.bz2", "unsat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_9nodes.abstract.base.smt2.bz2", "unsat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_8nodes.synchro.induct.smt2.bz2", "unsat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_4nodes.synchro.base.smt2.bz2", "unsat"),
(QF_LRA, "small_set/QF_LRA/simple_startup_14nodes.synchro.induct.smt2.bz2", "unsat"),
#
# LRA
#
(LRA, "small_set/LRA/water_tank-node21140.smt2.bz2", "unsat"),
(LRA, "small_set/LRA/water_tank-node22228.smt2.bz2", "unsat"),
(LRA, "small_set/LRA/water_tank-node9350.smt2.bz2", "unsat"),
(LRA, "small_set/LRA/intersection-example-simple.proof-node679466.smt2.bz2", "unsat"),
(LRA, "small_set/LRA/intersection-example-simple.proof-node394346.smt2.bz2", "unsat"),
(LRA, "small_set/LRA/water_tank-node24658.smt2.bz2", "unsat"),
#
# QF_LIRA
#
(QF_UFLIRA, "small_set/QF_LIRA/lira1.smt2.bz2", "sat"),
(QF_UFLIRA, "small_set/QF_LIRA/prp-20-46.smt2.bz2", "sat"),
#
# QF_UFBV
#
#(QF_UFBV, "small_set/QF_UFBV/btfnt_atlas_out.smt2.bz2", "unsat"),
(QF_UFBV, "small_set/QF_UFBV/calc2_sec2_bmc10.smt2.bz2", "unsat"),
(QF_BV, "small_set/QF_BV/bench_4631_simp.smt2.bz2", "sat"),
(QF_BV, "small_set/QF_BV/bench_5200.smt2.bz2", "unsat"),
(QF_BV, "small_set/QF_BV/bench_9457_simp.smt2.bz2", "sat"),
#
# Arrays
(QF_ABV, "small_set/QF_ABV/a268test0002.smt2.bz2", "sat"),
(QF_ABV, "small_set/QF_ABV/com.galois.ecc.P384ECC64.group_add6.short.smt2.bz2", "unsat"),

(QF_ALIA, "small_set/QF_ALIA/ios_t1_ios_np_sf_ai_00001_001.cvc.smt2.bz2", "unsat"),
(QF_ALIA, "small_set/QF_ALIA/pointer-invalid-15.smt2.bz2", "sat"),

(QF_AUFBV, "small_set/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div10.short.smt2.bz2", "unsat"),

(QF_AUFLIA, "small_set/QF_AUFLIA/array_incompleteness1.smt2.bz2", "unsat"),
(QF_AUFLIA, "small_set/QF_AUFLIA/swap_invalid_t1_pp_nf_ai_00002_002.cvc.smt2.bz2", "sat"),
#
# QF_NRA
#
(QF_NRA, "small_set/QF_NRA/ball_count_2d_hill_simple.05.redlog_global_6.smt2.bz2", "unsat"),
(QF_NRA, "small_set/QF_NRA/cos-problem-12-chunk-0004.smt2.bz2", "sat"),
(QF_NRA, "small_set/QF_NRA/simple_ballistics_reach.01.seq_lazy_linear_enc_global_10.smt2.bz2", "unsat"),
#
# QF_NIA
#
(QF_NIA, "small_set/QF_NIA/aproveSMT3509292547826641386.smt2.bz2", "sat"),
(QF_NIA, "small_set/QF_NIA/problem-000158.cvc.2.smt2.bz2", "unsat"),
(QF_NIA, "small_set/QF_NIA/term-DtOD2C.smt2.bz2", "sat"),
]

# We use test generation in order to be able to obtain a separate
# test for each file.
# This is a feature of nosetest. The correct way to invoke these
Expand All @@ -140,10 +53,7 @@ def execute_script_fname(smtfile, logic, expected_result):
raise

res = check_sat_filter(log)
if res:
assert expected_result == "sat"
else:
assert expected_result == "unsat"
assert expected_result == res


def formulas_from_smtlib_test_set(logics=None):
Expand All @@ -158,3 +68,105 @@ def formulas_from_smtlib_test_set(logics=None):
smtfile = os.path.join(SMTLIB_DIR, fname)
formula = get_formula_fname(smtfile)
yield (logic, fname, formula, expected_result)


# Constants to make definition of the benchmarks more readable
SAT = True
UNSAT = False

# Directory where SMT-LIB files are saved
SMTLIB_DIR = "pysmt/test/smtlib/"
SMTLIB_TEST_FILES = [
#
# QF_LIA
#
(QF_LIA, "small_set/QF_LIA/prp-23-47.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-20-46.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-24-47.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-24-46.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-22-46.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-25-49.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-21-46.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-23-46.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-25-48.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-25-47.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-24-48.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/prp-25-46.smt2.bz2", UNSAT),
(QF_LIA, "small_set/QF_LIA/issue_159.smt2.bz2", SAT),
#
# QF_LRA
#
(QF_LRA, "small_set/QF_LRA/uart-8.induction.cvc.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/uart-10.induction.cvc.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/uart-18.induction.cvc.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/uart-26.induction.cvc.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/uart-11.induction.cvc.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/uart-16.induction.cvc.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/uart-6.induction.cvc.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/uart-14.induction.cvc.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_11nodes.abstract.base.smt2.bz2", UNSAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_8nodes.synchro.base.smt2.bz2", UNSAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_3nodes.bug.induct.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_15nodes.abstract.base.smt2.bz2", UNSAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_12nodes.synchro.base.smt2.bz2", UNSAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_8nodes.missing.induct.smt2.bz2", SAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_14nodes.abstract.base.smt2.bz2", UNSAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_9nodes.abstract.base.smt2.bz2", UNSAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_8nodes.synchro.induct.smt2.bz2", UNSAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_4nodes.synchro.base.smt2.bz2", UNSAT),
(QF_LRA, "small_set/QF_LRA/simple_startup_14nodes.synchro.induct.smt2.bz2", UNSAT),
#
# LRA
#
(LRA, "small_set/LRA/water_tank-node21140.smt2.bz2", UNSAT),
(LRA, "small_set/LRA/water_tank-node22228.smt2.bz2", UNSAT),
(LRA, "small_set/LRA/water_tank-node9350.smt2.bz2", UNSAT),
(LRA, "small_set/LRA/intersection-example-simple.proof-node679466.smt2.bz2", UNSAT),
(LRA, "small_set/LRA/intersection-example-simple.proof-node394346.smt2.bz2", UNSAT),
(LRA, "small_set/LRA/water_tank-node24658.smt2.bz2", UNSAT),
#
# QF_LIRA
#
(QF_UFLIRA, "small_set/QF_LIRA/lira1.smt2.bz2", SAT),
(QF_UFLIRA, "small_set/QF_LIRA/prp-20-46.smt2.bz2", SAT),
#
# QF_UFBV
#
#(QF_UFBV, "small_set/QF_UFBV/btfnt_atlas_out.smt2.bz2", UNSAT),
(QF_UFBV, "small_set/QF_UFBV/calc2_sec2_bmc10.smt2.bz2", UNSAT),
(QF_BV, "small_set/QF_BV/bench_4631_simp.smt2.bz2", SAT),
(QF_BV, "small_set/QF_BV/bench_5200.smt2.bz2", UNSAT),
(QF_BV, "small_set/QF_BV/bench_9457_simp.smt2.bz2", SAT),
#
# UFBV
#
(BV, "small_set/BV/AR-fixpoint-1.smt2.bz2", UNSAT),
(BV, "small_set/BV/audio_ac97_common.cpp.smt2.bz2", SAT),
(UFBV, "small_set/UFBV/small-swap2-fixpoint-5.smt2.bz2", SAT),
(UFBV, "small_set/UFBV/small-seq-fixpoint-10.smt2.bz2", UNSAT),
#
# Arrays
#
(QF_ABV, "small_set/QF_ABV/a268test0002.smt2.bz2", SAT),
(QF_ABV, "small_set/QF_ABV/com.galois.ecc.P384ECC64.group_add6.short.smt2.bz2", UNSAT),

(QF_ALIA, "small_set/QF_ALIA/ios_t1_ios_np_sf_ai_00001_001.cvc.smt2.bz2", UNSAT),
(QF_ALIA, "small_set/QF_ALIA/pointer-invalid-15.smt2.bz2", SAT),

(QF_AUFBV, "small_set/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div10.short.smt2.bz2", UNSAT),

(QF_AUFLIA, "small_set/QF_AUFLIA/array_incompleteness1.smt2.bz2", UNSAT),
(QF_AUFLIA, "small_set/QF_AUFLIA/swap_invalid_t1_pp_nf_ai_00002_002.cvc.smt2.bz2", SAT),
#
# QF_NRA
#
(QF_NRA, "small_set/QF_NRA/ball_count_2d_hill_simple.05.redlog_global_6.smt2.bz2", UNSAT),
(QF_NRA, "small_set/QF_NRA/cos-problem-12-chunk-0004.smt2.bz2", SAT),
(QF_NRA, "small_set/QF_NRA/simple_ballistics_reach.01.seq_lazy_linear_enc_global_10.smt2.bz2", UNSAT),
#
# QF_NIA
#
(QF_NIA, "small_set/QF_NIA/aproveSMT3509292547826641386.smt2.bz2", SAT),
(QF_NIA, "small_set/QF_NIA/problem-000158.cvc.2.smt2.bz2", UNSAT),
(QF_NIA, "small_set/QF_NIA/term-DtOD2C.smt2.bz2", SAT),
]
Binary file added pysmt/test/smtlib/small_set/BV/AR-fixpoint-1.smt2.bz2
View file
Binary file not shown.
Binary file added pysmt/test/smtlib/small_set/BV/audio_ac97_common.cpp.smt2.bz2
View file
Binary file not shown.
Binary file added pysmt/test/smtlib/small_set/UFBV/small-seq-fixpoint-10.smt2.bz2
View file
Binary file not shown.
Binary file added pysmt/test/smtlib/small_set/UFBV/small-swap2-fixpoint-5.smt2.bz2
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion pysmt/test/test_cnf.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ def test_smtlib_cnf(self):
for (logic, f, expected_result) in SMTLIB_TEST_FILES:
if logic != QF_UFLIRA:
continue
self._smtlib_cnf(f, logic, expected_result=="sat")
self._smtlib_cnf(f, logic, expected_result)

def _smtlib_cnf(self, filename, logic, res_is_sat):
reset_env()
Expand Down
6 changes: 2 additions & 4 deletions pysmt/test/test_portfolio.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,7 @@ def test_smtlib_multi_msat(self):
incremental=False,
generate_models=False) as s:
res = s.is_sat(formula)
result = "sat" if res else "unsat"
self.assertEqual(expected_result, result, smtfile)
self.assertEqual(expected_result, res, smtfile)

def run_smtlib(self, smtfile, logic, expected_result):
env = reset_env()
Expand All @@ -84,8 +83,7 @@ def run_smtlib(self, smtfile, logic, expected_result):
incremental=False,
generate_models=False) as s:
res = s.is_sat(formula)
result = "sat" if res else "unsat"
self.assertEqual(expected_result, result, smtfile)
self.assertEqual(expected_result, res, smtfile)

@skipIfSolverNotAvailable("msat")
@skipIfSolverNotAvailable("cvc4")
Expand Down

0 comments on commit b4e6a59

Please sign in to comment.