Permalink
Browse files

Examples: parallel.py avoid Strings Theory

  • Loading branch information...
marcogario committed Nov 23, 2017
1 parent dfd7944 commit b3c244059eded8b885727f19b0991bc881754930
Showing with 5 additions and 2 deletions.
  1. +1 −0 examples/parallel.py
  2. +4 −2 pysmt/solvers/cvc4.py
View
@@ -94,6 +94,7 @@ def check_validity_and_test(args):
big_f = And(f.expr for f in get_example_formulae() \
if not f.logic.theory.bit_vectors and \
not f.logic.theory.arrays and \
not f.logic.theory.strings and \
f.logic.theory.linear)
# Create keyword arguments for the function call.
View
@@ -27,7 +27,7 @@
raise SolverAPINotFound
import pysmt.typing as types
from pysmt.logics import PYSMT_LOGICS, ARRAYS_CONST_LOGICS, QF_SLIA
from pysmt.logics import PYSMT_LOGICS, ARRAYS_CONST_LOGICS
from pysmt.solvers.solver import Solver, Converter, SolverOptions
from pysmt.exceptions import (SolverReturnedUnknownResultError,
@@ -78,8 +78,10 @@ def __call__(self, solver):
class CVC4Solver(Solver, SmtLibBasicSolver, SmtLibIgnoreMixin):
LOGICS = ( PYSMT_LOGICS | frozenset([QF_SLIA]) ) - ARRAYS_CONST_LOGICS -\
LOGICS = PYSMT_LOGICS -\
ARRAYS_CONST_LOGICS -\
set(l for l in PYSMT_LOGICS if not l.theory.linear)
OptionsClass = CVC4Options
def __init__(self, environment, logic, **options):

0 comments on commit b3c2440

Please sign in to comment.