chore: 添加虚拟环境到仓库
- 添加 backend_service/venv 虚拟环境 - 包含所有Python依赖包 - 注意：虚拟环境约393MB，包含12655个文件
This commit is contained in:
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,234 @@
|
||||
"""Various tests on satisfiability using dimacs cnf file syntax
|
||||
You can find lots of cnf files in
|
||||
ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/benchmarks/cnf/
|
||||
"""
|
||||
|
||||
from sympy.logic.utilities.dimacs import load
|
||||
from sympy.logic.algorithms.dpll import dpll_satisfiable
|
||||
|
||||
|
||||
def test_f1():
|
||||
assert bool(dpll_satisfiable(load(f1)))
|
||||
|
||||
|
||||
def test_f2():
|
||||
assert bool(dpll_satisfiable(load(f2)))
|
||||
|
||||
|
||||
def test_f3():
|
||||
assert bool(dpll_satisfiable(load(f3)))
|
||||
|
||||
|
||||
def test_f4():
|
||||
assert not bool(dpll_satisfiable(load(f4)))
|
||||
|
||||
|
||||
def test_f5():
|
||||
assert bool(dpll_satisfiable(load(f5)))
|
||||
|
||||
f1 = """c simple example
|
||||
c Resolution: SATISFIABLE
|
||||
c
|
||||
p cnf 3 2
|
||||
1 -3 0
|
||||
2 3 -1 0
|
||||
"""
|
||||
|
||||
|
||||
f2 = """c an example from Quinn's text, 16 variables and 18 clauses.
|
||||
c Resolution: SATISFIABLE
|
||||
c
|
||||
p cnf 16 18
|
||||
1 2 0
|
||||
-2 -4 0
|
||||
3 4 0
|
||||
-4 -5 0
|
||||
5 -6 0
|
||||
6 -7 0
|
||||
6 7 0
|
||||
7 -16 0
|
||||
8 -9 0
|
||||
-8 -14 0
|
||||
9 10 0
|
||||
9 -10 0
|
||||
-10 -11 0
|
||||
10 12 0
|
||||
11 12 0
|
||||
13 14 0
|
||||
14 -15 0
|
||||
15 16 0
|
||||
"""
|
||||
|
||||
f3 = """c
|
||||
p cnf 6 9
|
||||
-1 0
|
||||
-3 0
|
||||
2 -1 0
|
||||
2 -4 0
|
||||
5 -4 0
|
||||
-1 -3 0
|
||||
-4 -6 0
|
||||
1 3 -2 0
|
||||
4 6 -2 -5 0
|
||||
"""
|
||||
|
||||
f4 = """c
|
||||
c file: hole6.cnf [http://people.sc.fsu.edu/~jburkardt/data/cnf/hole6.cnf]
|
||||
c
|
||||
c SOURCE: John Hooker (jh38+@andrew.cmu.edu)
|
||||
c
|
||||
c DESCRIPTION: Pigeon hole problem of placing n (for file 'holen.cnf') pigeons
|
||||
c in n+1 holes without placing 2 pigeons in the same hole
|
||||
c
|
||||
c NOTE: Part of the collection at the Forschungsinstitut fuer
|
||||
c anwendungsorientierte Wissensverarbeitung in Ulm Germany.
|
||||
c
|
||||
c NOTE: Not satisfiable
|
||||
c
|
||||
p cnf 42 133
|
||||
-1 -7 0
|
||||
-1 -13 0
|
||||
-1 -19 0
|
||||
-1 -25 0
|
||||
-1 -31 0
|
||||
-1 -37 0
|
||||
-7 -13 0
|
||||
-7 -19 0
|
||||
-7 -25 0
|
||||
-7 -31 0
|
||||
-7 -37 0
|
||||
-13 -19 0
|
||||
-13 -25 0
|
||||
-13 -31 0
|
||||
-13 -37 0
|
||||
-19 -25 0
|
||||
-19 -31 0
|
||||
-19 -37 0
|
||||
-25 -31 0
|
||||
-25 -37 0
|
||||
-31 -37 0
|
||||
-2 -8 0
|
||||
-2 -14 0
|
||||
-2 -20 0
|
||||
-2 -26 0
|
||||
-2 -32 0
|
||||
-2 -38 0
|
||||
-8 -14 0
|
||||
-8 -20 0
|
||||
-8 -26 0
|
||||
-8 -32 0
|
||||
-8 -38 0
|
||||
-14 -20 0
|
||||
-14 -26 0
|
||||
-14 -32 0
|
||||
-14 -38 0
|
||||
-20 -26 0
|
||||
-20 -32 0
|
||||
-20 -38 0
|
||||
-26 -32 0
|
||||
-26 -38 0
|
||||
-32 -38 0
|
||||
-3 -9 0
|
||||
-3 -15 0
|
||||
-3 -21 0
|
||||
-3 -27 0
|
||||
-3 -33 0
|
||||
-3 -39 0
|
||||
-9 -15 0
|
||||
-9 -21 0
|
||||
-9 -27 0
|
||||
-9 -33 0
|
||||
-9 -39 0
|
||||
-15 -21 0
|
||||
-15 -27 0
|
||||
-15 -33 0
|
||||
-15 -39 0
|
||||
-21 -27 0
|
||||
-21 -33 0
|
||||
-21 -39 0
|
||||
-27 -33 0
|
||||
-27 -39 0
|
||||
-33 -39 0
|
||||
-4 -10 0
|
||||
-4 -16 0
|
||||
-4 -22 0
|
||||
-4 -28 0
|
||||
-4 -34 0
|
||||
-4 -40 0
|
||||
-10 -16 0
|
||||
-10 -22 0
|
||||
-10 -28 0
|
||||
-10 -34 0
|
||||
-10 -40 0
|
||||
-16 -22 0
|
||||
-16 -28 0
|
||||
-16 -34 0
|
||||
-16 -40 0
|
||||
-22 -28 0
|
||||
-22 -34 0
|
||||
-22 -40 0
|
||||
-28 -34 0
|
||||
-28 -40 0
|
||||
-34 -40 0
|
||||
-5 -11 0
|
||||
-5 -17 0
|
||||
-5 -23 0
|
||||
-5 -29 0
|
||||
-5 -35 0
|
||||
-5 -41 0
|
||||
-11 -17 0
|
||||
-11 -23 0
|
||||
-11 -29 0
|
||||
-11 -35 0
|
||||
-11 -41 0
|
||||
-17 -23 0
|
||||
-17 -29 0
|
||||
-17 -35 0
|
||||
-17 -41 0
|
||||
-23 -29 0
|
||||
-23 -35 0
|
||||
-23 -41 0
|
||||
-29 -35 0
|
||||
-29 -41 0
|
||||
-35 -41 0
|
||||
-6 -12 0
|
||||
-6 -18 0
|
||||
-6 -24 0
|
||||
-6 -30 0
|
||||
-6 -36 0
|
||||
-6 -42 0
|
||||
-12 -18 0
|
||||
-12 -24 0
|
||||
-12 -30 0
|
||||
-12 -36 0
|
||||
-12 -42 0
|
||||
-18 -24 0
|
||||
-18 -30 0
|
||||
-18 -36 0
|
||||
-18 -42 0
|
||||
-24 -30 0
|
||||
-24 -36 0
|
||||
-24 -42 0
|
||||
-30 -36 0
|
||||
-30 -42 0
|
||||
-36 -42 0
|
||||
6 5 4 3 2 1 0
|
||||
12 11 10 9 8 7 0
|
||||
18 17 16 15 14 13 0
|
||||
24 23 22 21 20 19 0
|
||||
30 29 28 27 26 25 0
|
||||
36 35 34 33 32 31 0
|
||||
42 41 40 39 38 37 0
|
||||
"""
|
||||
|
||||
f5 = """c simple example requiring variable selection
|
||||
c
|
||||
c NOTE: Satisfiable
|
||||
c
|
||||
p cnf 5 5
|
||||
1 2 3 0
|
||||
1 -2 3 0
|
||||
4 5 -3 0
|
||||
1 -4 -3 0
|
||||
-1 -5 0
|
||||
"""
|
||||
@@ -0,0 +1,396 @@
|
||||
"""For more tests on satisfiability, see test_dimacs"""
|
||||
|
||||
from sympy.assumptions.ask import Q
|
||||
from sympy.core.symbol import symbols
|
||||
from sympy.core.relational import Unequality
|
||||
from sympy.logic.boolalg import And, Or, Implies, Equivalent, true, false
|
||||
from sympy.logic.inference import literal_symbol, \
|
||||
pl_true, satisfiable, valid, entails, PropKB
|
||||
from sympy.logic.algorithms.dpll import dpll, dpll_satisfiable, \
|
||||
find_pure_symbol, find_unit_clause, unit_propagate, \
|
||||
find_pure_symbol_int_repr, find_unit_clause_int_repr, \
|
||||
unit_propagate_int_repr
|
||||
from sympy.logic.algorithms.dpll2 import dpll_satisfiable as dpll2_satisfiable
|
||||
|
||||
from sympy.logic.algorithms.z3_wrapper import z3_satisfiable
|
||||
from sympy.assumptions.cnf import CNF, EncodedCNF
|
||||
from sympy.logic.tests.test_lra_theory import make_random_problem
|
||||
from sympy.core.random import randint
|
||||
|
||||
from sympy.testing.pytest import raises, skip
|
||||
from sympy.external import import_module
|
||||
|
||||
|
||||
def test_literal():
|
||||
A, B = symbols('A,B')
|
||||
assert literal_symbol(True) is True
|
||||
assert literal_symbol(False) is False
|
||||
assert literal_symbol(A) is A
|
||||
assert literal_symbol(~A) is A
|
||||
|
||||
|
||||
def test_find_pure_symbol():
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert find_pure_symbol([A], [A]) == (A, True)
|
||||
assert find_pure_symbol([A, B], [~A | B, ~B | A]) == (None, None)
|
||||
assert find_pure_symbol([A, B, C], [ A | ~B, ~B | ~C, C | A]) == (A, True)
|
||||
assert find_pure_symbol([A, B, C], [~A | B, B | ~C, C | A]) == (B, True)
|
||||
assert find_pure_symbol([A, B, C], [~A | ~B, ~B | ~C, C | A]) == (B, False)
|
||||
assert find_pure_symbol(
|
||||
[A, B, C], [~A | B, ~B | ~C, C | A]) == (None, None)
|
||||
|
||||
|
||||
def test_find_pure_symbol_int_repr():
|
||||
assert find_pure_symbol_int_repr([1], [{1}]) == (1, True)
|
||||
assert find_pure_symbol_int_repr([1, 2],
|
||||
[{-1, 2}, {-2, 1}]) == (None, None)
|
||||
assert find_pure_symbol_int_repr([1, 2, 3],
|
||||
[{1, -2}, {-2, -3}, {3, 1}]) == (1, True)
|
||||
assert find_pure_symbol_int_repr([1, 2, 3],
|
||||
[{-1, 2}, {2, -3}, {3, 1}]) == (2, True)
|
||||
assert find_pure_symbol_int_repr([1, 2, 3],
|
||||
[{-1, -2}, {-2, -3}, {3, 1}]) == (2, False)
|
||||
assert find_pure_symbol_int_repr([1, 2, 3],
|
||||
[{-1, 2}, {-2, -3}, {3, 1}]) == (None, None)
|
||||
|
||||
|
||||
def test_unit_clause():
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert find_unit_clause([A], {}) == (A, True)
|
||||
assert find_unit_clause([A, ~A], {}) == (A, True) # Wrong ??
|
||||
assert find_unit_clause([A | B], {A: True}) == (B, True)
|
||||
assert find_unit_clause([A | B], {B: True}) == (A, True)
|
||||
assert find_unit_clause(
|
||||
[A | B | C, B | ~C, A | ~B], {A: True}) == (B, False)
|
||||
assert find_unit_clause([A | B | C, B | ~C, A | B], {A: True}) == (B, True)
|
||||
assert find_unit_clause([A | B | C, B | ~C, A ], {}) == (A, True)
|
||||
|
||||
|
||||
def test_unit_clause_int_repr():
|
||||
assert find_unit_clause_int_repr(map(set, [[1]]), {}) == (1, True)
|
||||
assert find_unit_clause_int_repr(map(set, [[1], [-1]]), {}) == (1, True)
|
||||
assert find_unit_clause_int_repr([{1, 2}], {1: True}) == (2, True)
|
||||
assert find_unit_clause_int_repr([{1, 2}], {2: True}) == (1, True)
|
||||
assert find_unit_clause_int_repr(map(set,
|
||||
[[1, 2, 3], [2, -3], [1, -2]]), {1: True}) == (2, False)
|
||||
assert find_unit_clause_int_repr(map(set,
|
||||
[[1, 2, 3], [3, -3], [1, 2]]), {1: True}) == (2, True)
|
||||
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert find_unit_clause([A | B | C, B | ~C, A ], {}) == (A, True)
|
||||
|
||||
|
||||
def test_unit_propagate():
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert unit_propagate([A | B], A) == []
|
||||
assert unit_propagate([A | B, ~A | C, ~C | B, A], A) == [C, ~C | B, A]
|
||||
|
||||
|
||||
def test_unit_propagate_int_repr():
|
||||
assert unit_propagate_int_repr([{1, 2}], 1) == []
|
||||
assert unit_propagate_int_repr(map(set,
|
||||
[[1, 2], [-1, 3], [-3, 2], [1]]), 1) == [{3}, {-3, 2}]
|
||||
|
||||
|
||||
def test_dpll():
|
||||
"""This is also tested in test_dimacs"""
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert dpll([A | B], [A, B], {A: True, B: True}) == {A: True, B: True}
|
||||
|
||||
|
||||
def test_dpll_satisfiable():
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert dpll_satisfiable( A & ~A ) is False
|
||||
assert dpll_satisfiable( A & ~B ) == {A: True, B: False}
|
||||
assert dpll_satisfiable(
|
||||
A | B ) in ({A: True}, {B: True}, {A: True, B: True})
|
||||
assert dpll_satisfiable(
|
||||
(~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B: False})
|
||||
assert dpll_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False},
|
||||
{A: True, C: True}, {B: True, C: True})
|
||||
assert dpll_satisfiable( A & B & C ) == {A: True, B: True, C: True}
|
||||
assert dpll_satisfiable( (A | B) & (A >> B) ) == {B: True}
|
||||
assert dpll_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
|
||||
assert dpll_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}
|
||||
|
||||
|
||||
def test_dpll2_satisfiable():
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert dpll2_satisfiable( A & ~A ) is False
|
||||
assert dpll2_satisfiable( A & ~B ) == {A: True, B: False}
|
||||
assert dpll2_satisfiable(
|
||||
A | B ) in ({A: True}, {B: True}, {A: True, B: True})
|
||||
assert dpll2_satisfiable(
|
||||
(~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B: False})
|
||||
assert dpll2_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False, C: True},
|
||||
{A: True, B: True, C: True})
|
||||
assert dpll2_satisfiable( A & B & C ) == {A: True, B: True, C: True}
|
||||
assert dpll2_satisfiable( (A | B) & (A >> B) ) in ({B: True, A: False},
|
||||
{B: True, A: True})
|
||||
assert dpll2_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
|
||||
assert dpll2_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}
|
||||
|
||||
|
||||
def test_minisat22_satisfiable():
|
||||
A, B, C = symbols('A,B,C')
|
||||
minisat22_satisfiable = lambda expr: satisfiable(expr, algorithm="minisat22")
|
||||
assert minisat22_satisfiable( A & ~A ) is False
|
||||
assert minisat22_satisfiable( A & ~B ) == {A: True, B: False}
|
||||
assert minisat22_satisfiable(
|
||||
A | B ) in ({A: True}, {B: False}, {A: False, B: True}, {A: True, B: True}, {A: True, B: False})
|
||||
assert minisat22_satisfiable(
|
||||
(~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B: False})
|
||||
assert minisat22_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False, C: True},
|
||||
{A: True, B: True, C: True}, {A: False, B: True, C: True}, {A: True, B: False, C: False})
|
||||
assert minisat22_satisfiable( A & B & C ) == {A: True, B: True, C: True}
|
||||
assert minisat22_satisfiable( (A | B) & (A >> B) ) in ({B: True, A: False},
|
||||
{B: True, A: True})
|
||||
assert minisat22_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
|
||||
assert minisat22_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}
|
||||
|
||||
def test_minisat22_minimal_satisfiable():
|
||||
A, B, C = symbols('A,B,C')
|
||||
minisat22_satisfiable = lambda expr, minimal=True: satisfiable(expr, algorithm="minisat22", minimal=True)
|
||||
assert minisat22_satisfiable( A & ~A ) is False
|
||||
assert minisat22_satisfiable( A & ~B ) == {A: True, B: False}
|
||||
assert minisat22_satisfiable(
|
||||
A | B ) in ({A: True}, {B: False}, {A: False, B: True}, {A: True, B: True}, {A: True, B: False})
|
||||
assert minisat22_satisfiable(
|
||||
(~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B: False})
|
||||
assert minisat22_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False, C: True},
|
||||
{A: True, B: True, C: True}, {A: False, B: True, C: True}, {A: True, B: False, C: False})
|
||||
assert minisat22_satisfiable( A & B & C ) == {A: True, B: True, C: True}
|
||||
assert minisat22_satisfiable( (A | B) & (A >> B) ) in ({B: True, A: False},
|
||||
{B: True, A: True})
|
||||
assert minisat22_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
|
||||
assert minisat22_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}
|
||||
g = satisfiable((A | B | C),algorithm="minisat22",minimal=True,all_models=True)
|
||||
sol = next(g)
|
||||
first_solution = {key for key, value in sol.items() if value}
|
||||
sol=next(g)
|
||||
second_solution = {key for key, value in sol.items() if value}
|
||||
sol=next(g)
|
||||
third_solution = {key for key, value in sol.items() if value}
|
||||
assert not first_solution <= second_solution
|
||||
assert not second_solution <= third_solution
|
||||
assert not first_solution <= third_solution
|
||||
|
||||
def test_satisfiable():
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert satisfiable(A & (A >> B) & ~B) is False
|
||||
|
||||
|
||||
def test_valid():
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert valid(A >> (B >> A)) is True
|
||||
assert valid((A >> (B >> C)) >> ((A >> B) >> (A >> C))) is True
|
||||
assert valid((~B >> ~A) >> (A >> B)) is True
|
||||
assert valid(A | B | C) is False
|
||||
assert valid(A >> B) is False
|
||||
|
||||
|
||||
def test_pl_true():
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert pl_true(True) is True
|
||||
assert pl_true( A & B, {A: True, B: True}) is True
|
||||
assert pl_true( A | B, {A: True}) is True
|
||||
assert pl_true( A | B, {B: True}) is True
|
||||
assert pl_true( A | B, {A: None, B: True}) is True
|
||||
assert pl_true( A >> B, {A: False}) is True
|
||||
assert pl_true( A | B | ~C, {A: False, B: True, C: True}) is True
|
||||
assert pl_true(Equivalent(A, B), {A: False, B: False}) is True
|
||||
|
||||
# test for false
|
||||
assert pl_true(False) is False
|
||||
assert pl_true( A & B, {A: False, B: False}) is False
|
||||
assert pl_true( A & B, {A: False}) is False
|
||||
assert pl_true( A & B, {B: False}) is False
|
||||
assert pl_true( A | B, {A: False, B: False}) is False
|
||||
|
||||
#test for None
|
||||
assert pl_true(B, {B: None}) is None
|
||||
assert pl_true( A & B, {A: True, B: None}) is None
|
||||
assert pl_true( A >> B, {A: True, B: None}) is None
|
||||
assert pl_true(Equivalent(A, B), {A: None}) is None
|
||||
assert pl_true(Equivalent(A, B), {A: True, B: None}) is None
|
||||
|
||||
# Test for deep
|
||||
assert pl_true(A | B, {A: False}, deep=True) is None
|
||||
assert pl_true(~A & ~B, {A: False}, deep=True) is None
|
||||
assert pl_true(A | B, {A: False, B: False}, deep=True) is False
|
||||
assert pl_true(A & B & (~A | ~B), {A: True}, deep=True) is False
|
||||
assert pl_true((C >> A) >> (B >> A), {C: True}, deep=True) is True
|
||||
|
||||
|
||||
def test_pl_true_wrong_input():
|
||||
from sympy.core.numbers import pi
|
||||
raises(ValueError, lambda: pl_true('John Cleese'))
|
||||
raises(ValueError, lambda: pl_true(42 + pi + pi ** 2))
|
||||
raises(ValueError, lambda: pl_true(42))
|
||||
|
||||
|
||||
def test_entails():
|
||||
A, B, C = symbols('A, B, C')
|
||||
assert entails(A, [A >> B, ~B]) is False
|
||||
assert entails(B, [Equivalent(A, B), A]) is True
|
||||
assert entails((A >> B) >> (~A >> ~B)) is False
|
||||
assert entails((A >> B) >> (~B >> ~A)) is True
|
||||
|
||||
|
||||
def test_PropKB():
|
||||
A, B, C = symbols('A,B,C')
|
||||
kb = PropKB()
|
||||
assert kb.ask(A >> B) is False
|
||||
assert kb.ask(A >> (B >> A)) is True
|
||||
kb.tell(A >> B)
|
||||
kb.tell(B >> C)
|
||||
assert kb.ask(A) is False
|
||||
assert kb.ask(B) is False
|
||||
assert kb.ask(C) is False
|
||||
assert kb.ask(~A) is False
|
||||
assert kb.ask(~B) is False
|
||||
assert kb.ask(~C) is False
|
||||
assert kb.ask(A >> C) is True
|
||||
kb.tell(A)
|
||||
assert kb.ask(A) is True
|
||||
assert kb.ask(B) is True
|
||||
assert kb.ask(C) is True
|
||||
assert kb.ask(~C) is False
|
||||
kb.retract(A)
|
||||
assert kb.ask(C) is False
|
||||
|
||||
|
||||
def test_propKB_tolerant():
|
||||
""""tolerant to bad input"""
|
||||
kb = PropKB()
|
||||
A, B, C = symbols('A,B,C')
|
||||
assert kb.ask(B) is False
|
||||
|
||||
def test_satisfiable_non_symbols():
|
||||
x, y = symbols('x y')
|
||||
assumptions = Q.zero(x*y)
|
||||
facts = Implies(Q.zero(x*y), Q.zero(x) | Q.zero(y))
|
||||
query = ~Q.zero(x) & ~Q.zero(y)
|
||||
refutations = [
|
||||
{Q.zero(x): True, Q.zero(x*y): True},
|
||||
{Q.zero(y): True, Q.zero(x*y): True},
|
||||
{Q.zero(x): True, Q.zero(y): True, Q.zero(x*y): True},
|
||||
{Q.zero(x): True, Q.zero(y): False, Q.zero(x*y): True},
|
||||
{Q.zero(x): False, Q.zero(y): True, Q.zero(x*y): True}]
|
||||
assert not satisfiable(And(assumptions, facts, query), algorithm='dpll')
|
||||
assert satisfiable(And(assumptions, facts, ~query), algorithm='dpll') in refutations
|
||||
assert not satisfiable(And(assumptions, facts, query), algorithm='dpll2')
|
||||
assert satisfiable(And(assumptions, facts, ~query), algorithm='dpll2') in refutations
|
||||
|
||||
def test_satisfiable_bool():
|
||||
from sympy.core.singleton import S
|
||||
assert satisfiable(true) == {true: true}
|
||||
assert satisfiable(S.true) == {true: true}
|
||||
assert satisfiable(false) is False
|
||||
assert satisfiable(S.false) is False
|
||||
|
||||
|
||||
def test_satisfiable_all_models():
|
||||
from sympy.abc import A, B
|
||||
assert next(satisfiable(False, all_models=True)) is False
|
||||
assert list(satisfiable((A >> ~A) & A, all_models=True)) == [False]
|
||||
assert list(satisfiable(True, all_models=True)) == [{true: true}]
|
||||
|
||||
models = [{A: True, B: False}, {A: False, B: True}]
|
||||
result = satisfiable(A ^ B, all_models=True)
|
||||
models.remove(next(result))
|
||||
models.remove(next(result))
|
||||
raises(StopIteration, lambda: next(result))
|
||||
assert not models
|
||||
|
||||
assert list(satisfiable(Equivalent(A, B), all_models=True)) == \
|
||||
[{A: False, B: False}, {A: True, B: True}]
|
||||
|
||||
models = [{A: False, B: False}, {A: False, B: True}, {A: True, B: True}]
|
||||
for model in satisfiable(A >> B, all_models=True):
|
||||
models.remove(model)
|
||||
assert not models
|
||||
|
||||
# This is a santiy test to check that only the required number
|
||||
# of solutions are generated. The expr below has 2**100 - 1 models
|
||||
# which would time out the test if all are generated at once.
|
||||
from sympy.utilities.iterables import numbered_symbols
|
||||
from sympy.logic.boolalg import Or
|
||||
sym = numbered_symbols()
|
||||
X = [next(sym) for i in range(100)]
|
||||
result = satisfiable(Or(*X), all_models=True)
|
||||
for i in range(10):
|
||||
assert next(result)
|
||||
|
||||
|
||||
def test_z3():
|
||||
z3 = import_module("z3")
|
||||
|
||||
if not z3:
|
||||
skip("z3 not installed.")
|
||||
A, B, C = symbols('A,B,C')
|
||||
x, y, z = symbols('x,y,z')
|
||||
assert z3_satisfiable((x >= 2) & (x < 1)) is False
|
||||
assert z3_satisfiable( A & ~A ) is False
|
||||
|
||||
model = z3_satisfiable(A & (~A | B | C))
|
||||
assert bool(model) is True
|
||||
assert model[A] is True
|
||||
|
||||
# test nonlinear function
|
||||
assert z3_satisfiable((x ** 2 >= 2) & (x < 1) & (x > -1)) is False
|
||||
|
||||
|
||||
def test_z3_vs_lra_dpll2():
|
||||
z3 = import_module("z3")
|
||||
if z3 is None:
|
||||
skip("z3 not installed.")
|
||||
|
||||
def boolean_formula_to_encoded_cnf(bf):
|
||||
cnf = CNF.from_prop(bf)
|
||||
enc = EncodedCNF()
|
||||
enc.from_cnf(cnf)
|
||||
return enc
|
||||
|
||||
def make_random_cnf(num_clauses=5, num_constraints=10, num_var=2):
|
||||
assert num_clauses <= num_constraints
|
||||
constraints = make_random_problem(num_variables=num_var, num_constraints=num_constraints, rational=False)
|
||||
clauses = [[cons] for cons in constraints[:num_clauses]]
|
||||
for cons in constraints[num_clauses:]:
|
||||
if isinstance(cons, Unequality):
|
||||
cons = ~cons
|
||||
i = randint(0, num_clauses-1)
|
||||
clauses[i].append(cons)
|
||||
|
||||
clauses = [Or(*clause) for clause in clauses]
|
||||
cnf = And(*clauses)
|
||||
return boolean_formula_to_encoded_cnf(cnf)
|
||||
|
||||
lra_dpll2_satisfiable = lambda x: dpll2_satisfiable(x, use_lra_theory=True)
|
||||
|
||||
for _ in range(50):
|
||||
cnf = make_random_cnf(num_clauses=10, num_constraints=15, num_var=2)
|
||||
|
||||
try:
|
||||
z3_sat = z3_satisfiable(cnf)
|
||||
except z3.z3types.Z3Exception:
|
||||
continue
|
||||
|
||||
lra_dpll2_sat = lra_dpll2_satisfiable(cnf) is not False
|
||||
|
||||
assert z3_sat == lra_dpll2_sat
|
||||
|
||||
def test_issue_27733():
|
||||
x, y = symbols('x,y')
|
||||
clauses = [[1, -3, -2], [5, 7, -8, -6, -4], [-10, -9, 10, 11, -4], [-12, 13, 14], [-10, 9, -6, 11, -4],
|
||||
[16, -15, 18, -19, -17], [11, -6, 10, -9], [9, 11, -10, -9], [2, -3, -1], [-13, 12], [-15, 3, -17],
|
||||
[-16, -15, 19, -17], [-6, -9, 10, 11, -4], [20, -1, -2], [-23, -22, -21], [10, 11, -10, -9],
|
||||
[9, 11, -4, -10], [24, -6, -4], [-14, 12], [-10, -9, 9, -6, 11], [25, -27, -26], [-15, 19, -18, -17],
|
||||
[5, 8, -7, -6, -4], [-30, -29, 28], [12], [14]]
|
||||
|
||||
encoding = {Q.gt(y, i): i for i in range(1, 31) if i != 11 and i != 12}
|
||||
encoding[Q.gt(x, 0)] = 11
|
||||
encoding[Q.lt(x, 0)] = 12
|
||||
|
||||
cnf = EncodedCNF(clauses, encoding)
|
||||
assert satisfiable(cnf, use_lra_theory=True) is False
|
||||
@@ -0,0 +1,440 @@
|
||||
from sympy.core.numbers import Rational, I, oo
|
||||
from sympy.core.relational import Eq
|
||||
from sympy.core.symbol import symbols
|
||||
from sympy.core.singleton import S
|
||||
from sympy.matrices.dense import Matrix
|
||||
from sympy.matrices.dense import randMatrix
|
||||
from sympy.assumptions.ask import Q
|
||||
from sympy.logic.boolalg import And
|
||||
from sympy.abc import x, y, z
|
||||
from sympy.assumptions.cnf import CNF, EncodedCNF
|
||||
from sympy.functions.elementary.trigonometric import cos
|
||||
from sympy.external import import_module
|
||||
|
||||
from sympy.logic.algorithms.lra_theory import LRASolver, UnhandledInput, LRARational, HANDLE_NEGATION
|
||||
from sympy.core.random import random, choice, randint
|
||||
from sympy.core.sympify import sympify
|
||||
from sympy.ntheory.generate import randprime
|
||||
from sympy.core.relational import StrictLessThan, StrictGreaterThan
|
||||
import itertools
|
||||
|
||||
from sympy.testing.pytest import raises, XFAIL, skip
|
||||
|
||||
def make_random_problem(num_variables=2, num_constraints=2, sparsity=.1, rational=True,
|
||||
disable_strict = False, disable_nonstrict=False, disable_equality=False):
|
||||
def rand(sparsity=sparsity):
|
||||
if random() < sparsity:
|
||||
return sympify(0)
|
||||
if rational:
|
||||
int1, int2 = [randprime(0, 50) for _ in range(2)]
|
||||
return Rational(int1, int2) * choice([-1, 1])
|
||||
else:
|
||||
return randint(1, 10) * choice([-1, 1])
|
||||
|
||||
variables = symbols('x1:%s' % (num_variables + 1))
|
||||
constraints = []
|
||||
for _ in range(num_constraints):
|
||||
lhs, rhs = sum(rand() * x for x in variables), rand(sparsity=0) # sparsity=0 bc of bug with smtlib_code
|
||||
options = []
|
||||
if not disable_equality:
|
||||
options += [Eq(lhs, rhs)]
|
||||
if not disable_nonstrict:
|
||||
options += [lhs <= rhs, lhs >= rhs]
|
||||
if not disable_strict:
|
||||
options += [lhs < rhs, lhs > rhs]
|
||||
|
||||
constraints.append(choice(options))
|
||||
|
||||
return constraints
|
||||
|
||||
def check_if_satisfiable_with_z3(constraints):
|
||||
from sympy.external.importtools import import_module
|
||||
from sympy.printing.smtlib import smtlib_code
|
||||
from sympy.logic.boolalg import And
|
||||
boolean_formula = And(*constraints)
|
||||
z3 = import_module("z3")
|
||||
if z3:
|
||||
smtlib_string = smtlib_code(boolean_formula)
|
||||
s = z3.Solver()
|
||||
s.from_string(smtlib_string)
|
||||
res = str(s.check())
|
||||
if res == 'sat':
|
||||
return True
|
||||
elif res == 'unsat':
|
||||
return False
|
||||
else:
|
||||
raise ValueError(f"z3 was not able to check the satisfiability of {boolean_formula}")
|
||||
|
||||
def find_rational_assignment(constr, assignment, iter=20):
|
||||
eps = sympify(1)
|
||||
|
||||
for _ in range(iter):
|
||||
assign = {key: val[0] + val[1]*eps for key, val in assignment.items()}
|
||||
try:
|
||||
for cons in constr:
|
||||
assert cons.subs(assign) == True
|
||||
return assign
|
||||
except AssertionError:
|
||||
eps = eps/2
|
||||
|
||||
return None
|
||||
|
||||
def boolean_formula_to_encoded_cnf(bf):
|
||||
cnf = CNF.from_prop(bf)
|
||||
enc = EncodedCNF()
|
||||
enc.from_cnf(cnf)
|
||||
return enc
|
||||
|
||||
|
||||
def test_from_encoded_cnf():
|
||||
s1, s2 = symbols("s1 s2")
|
||||
|
||||
# Test preprocessing
|
||||
# Example is from section 3 of paper.
|
||||
phi = (x >= 0) & ((x + y <= 2) | (x + 2 * y - z >= 6)) & (Eq(x + y, 2) | (x + 2 * y - z > 4))
|
||||
enc = boolean_formula_to_encoded_cnf(phi)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
assert lra.A.shape == (2, 5)
|
||||
assert str(lra.slack) == '[_s1, _s2]'
|
||||
assert str(lra.nonslack) == '[x, y, z]'
|
||||
assert lra.A == Matrix([[ 1, 1, 0, -1, 0],
|
||||
[-1, -2, 1, 0, -1]])
|
||||
assert {(str(b.var), b.bound, b.upper, b.equality, b.strict) for b in lra.enc_to_boundary.values()} == {('_s1', 2, None, True, False),
|
||||
('_s1', 2, True, False, False),
|
||||
('_s2', -4, True, False, True),
|
||||
('_s2', -6, True, False, False),
|
||||
('x', 0, False, False, False)}
|
||||
|
||||
|
||||
def test_problem():
|
||||
from sympy.logic.algorithms.lra_theory import LRASolver
|
||||
from sympy.assumptions.cnf import CNF, EncodedCNF
|
||||
cons = [-2 * x - 2 * y >= 7, -9 * y >= 7, -6 * y >= 5]
|
||||
cnf = CNF().from_prop(And(*cons))
|
||||
enc = EncodedCNF()
|
||||
enc.from_cnf(cnf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc)
|
||||
lra.assert_lit(1)
|
||||
lra.assert_lit(2)
|
||||
lra.assert_lit(3)
|
||||
is_sat, assignment = lra.check()
|
||||
assert is_sat is True
|
||||
|
||||
|
||||
def test_random_problems():
|
||||
z3 = import_module("z3")
|
||||
if z3 is None:
|
||||
skip("z3 is not installed")
|
||||
|
||||
special_cases = []; x1, x2, x3 = symbols("x1 x2 x3")
|
||||
special_cases.append([x1 - 3 * x2 <= -5, 6 * x1 + 4 * x2 <= 0, -7 * x1 + 3 * x2 <= 3])
|
||||
special_cases.append([-3 * x1 >= 3, Eq(4 * x1, -1)])
|
||||
special_cases.append([-4 * x1 < 4, 6 * x1 <= -6])
|
||||
special_cases.append([-3 * x2 >= 7, 6 * x1 <= -5, -3 * x2 <= -4])
|
||||
special_cases.append([x + y >= 2, x + y <= 1])
|
||||
special_cases.append([x >= 0, x + y <= 2, x + 2 * y - z >= 6]) # from paper example
|
||||
special_cases.append([-2 * x1 - 2 * x2 >= 7, -9 * x1 >= 7, -6 * x1 >= 5])
|
||||
special_cases.append([2 * x1 > -3, -9 * x1 < -6, 9 * x1 <= 6])
|
||||
special_cases.append([-2*x1 < -4, 9*x1 > -9])
|
||||
special_cases.append([-6*x1 >= -1, -8*x1 + x2 >= 5, -8*x1 + 7*x2 < 4, x1 > 7])
|
||||
special_cases.append([Eq(x1, 2), Eq(5*x1, -2), Eq(-7*x2, -6), Eq(9*x1 + 10*x2, 9)])
|
||||
special_cases.append([Eq(3*x1, 6), Eq(x1 - 8*x2, -9), Eq(-7*x1 + 5*x2, 3), Eq(3*x2, 7)])
|
||||
special_cases.append([-4*x1 < 4, 6*x1 <= -6])
|
||||
special_cases.append([-3*x1 + 8*x2 >= -8, -10*x2 > 9, 8*x1 - 4*x2 < 8, 10*x1 - 9*x2 >= -9])
|
||||
special_cases.append([x1 + 5*x2 >= -6, 9*x1 - 3*x2 >= -9, 6*x1 + 6*x2 < -10, -3*x1 + 3*x2 < -7])
|
||||
special_cases.append([-9*x1 < 7, -5*x1 - 7*x2 < -1, 3*x1 + 7*x2 > 1, -6*x1 - 6*x2 > 9])
|
||||
special_cases.append([9*x1 - 6*x2 >= -7, 9*x1 + 4*x2 < -8, -7*x2 <= 1, 10*x2 <= -7])
|
||||
|
||||
feasible_count = 0
|
||||
for i in range(50):
|
||||
if i % 8 == 0:
|
||||
constraints = make_random_problem(num_variables=1, num_constraints=2, rational=False)
|
||||
elif i % 8 == 1:
|
||||
constraints = make_random_problem(num_variables=2, num_constraints=4, rational=False, disable_equality=True,
|
||||
disable_nonstrict=True)
|
||||
elif i % 8 == 2:
|
||||
constraints = make_random_problem(num_variables=2, num_constraints=4, rational=False, disable_strict=True)
|
||||
elif i % 8 == 3:
|
||||
constraints = make_random_problem(num_variables=3, num_constraints=12, rational=False)
|
||||
else:
|
||||
constraints = make_random_problem(num_variables=3, num_constraints=6, rational=False)
|
||||
|
||||
if i < len(special_cases):
|
||||
constraints = special_cases[i]
|
||||
|
||||
if False in constraints or True in constraints:
|
||||
continue
|
||||
|
||||
phi = And(*constraints)
|
||||
if phi == False:
|
||||
continue
|
||||
cnf = CNF.from_prop(phi); enc = EncodedCNF()
|
||||
enc.from_cnf(cnf)
|
||||
assert all(0 not in clause for clause in enc.data)
|
||||
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
s_subs = lra.s_subs
|
||||
|
||||
lra.run_checks = True
|
||||
s_subs_rev = {value: key for key, value in s_subs.items()}
|
||||
lits = {lit for clause in enc.data for lit in clause}
|
||||
|
||||
bounds = [(lra.enc_to_boundary[l], l) for l in lits if l in lra.enc_to_boundary]
|
||||
bounds = sorted(bounds, key=lambda x: (str(x[0].var), x[0].bound, str(x[0].upper))) # to remove nondeterminism
|
||||
|
||||
for b, l in bounds:
|
||||
if lra.result and lra.result[0] == False:
|
||||
break
|
||||
lra.assert_lit(l)
|
||||
|
||||
feasible = lra.check()
|
||||
|
||||
if feasible[0] == True:
|
||||
feasible_count += 1
|
||||
assert check_if_satisfiable_with_z3(constraints) is True
|
||||
cons_funcs = [cons.func for cons in constraints]
|
||||
assignment = feasible[1]
|
||||
assignment = {key.var : value for key, value in assignment.items()}
|
||||
if not (StrictLessThan in cons_funcs or StrictGreaterThan in cons_funcs):
|
||||
assignment = {key: value[0] for key, value in assignment.items()}
|
||||
for cons in constraints:
|
||||
assert cons.subs(assignment) == True
|
||||
|
||||
else:
|
||||
rat_assignment = find_rational_assignment(constraints, assignment)
|
||||
assert rat_assignment is not None
|
||||
else:
|
||||
assert check_if_satisfiable_with_z3(constraints) is False
|
||||
|
||||
conflict = feasible[1]
|
||||
assert len(conflict) >= 2
|
||||
conflict = {lra.enc_to_boundary[-l].get_inequality() for l in conflict}
|
||||
conflict = {clause.subs(s_subs_rev) for clause in conflict}
|
||||
assert check_if_satisfiable_with_z3(conflict) is False
|
||||
|
||||
# check that conflict clause is probably minimal
|
||||
for subset in itertools.combinations(conflict, len(conflict)-1):
|
||||
assert check_if_satisfiable_with_z3(subset) is True
|
||||
|
||||
|
||||
@XFAIL
|
||||
def test_pos_neg_zero():
|
||||
bf = Q.positive(x) & Q.negative(x) & Q.zero(y)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for lit in enc.encoding.values():
|
||||
if lra.assert_lit(lit) is not None:
|
||||
break
|
||||
assert len(lra.enc_to_boundary) == 3
|
||||
assert lra.check()[0] == False
|
||||
|
||||
bf = Q.positive(x) & Q.lt(x, -1)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for lit in enc.encoding.values():
|
||||
if lra.assert_lit(lit) is not None:
|
||||
break
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == False
|
||||
|
||||
bf = Q.positive(x) & Q.zero(x)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for lit in enc.encoding.values():
|
||||
if lra.assert_lit(lit) is not None:
|
||||
break
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == False
|
||||
|
||||
bf = Q.positive(x) & Q.zero(y)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for lit in enc.encoding.values():
|
||||
if lra.assert_lit(lit) is not None:
|
||||
break
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == True
|
||||
|
||||
|
||||
@XFAIL
|
||||
def test_pos_neg_infinite():
|
||||
bf = Q.positive_infinite(x) & Q.lt(x, 10000000) & Q.positive_infinite(y)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for lit in enc.encoding.values():
|
||||
if lra.assert_lit(lit) is not None:
|
||||
break
|
||||
assert len(lra.enc_to_boundary) == 3
|
||||
assert lra.check()[0] == False
|
||||
|
||||
bf = Q.positive_infinite(x) & Q.gt(x, 10000000) & Q.positive_infinite(y)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for lit in enc.encoding.values():
|
||||
if lra.assert_lit(lit) is not None:
|
||||
break
|
||||
assert len(lra.enc_to_boundary) == 3
|
||||
assert lra.check()[0] == True
|
||||
|
||||
bf = Q.positive_infinite(x) & Q.negative_infinite(x)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for lit in enc.encoding.values():
|
||||
if lra.assert_lit(lit) is not None:
|
||||
break
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == False
|
||||
|
||||
|
||||
def test_binrel_evaluation():
|
||||
bf = Q.gt(3, 2)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, conflicts = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
assert len(lra.enc_to_boundary) == 0
|
||||
assert conflicts == [[1]]
|
||||
|
||||
bf = Q.lt(3, 2)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, conflicts = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
assert len(lra.enc_to_boundary) == 0
|
||||
assert conflicts == [[-1]]
|
||||
|
||||
|
||||
def test_negation():
|
||||
assert HANDLE_NEGATION is True
|
||||
bf = Q.gt(x, 1) & ~Q.gt(x, 0)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for clause in enc.data:
|
||||
for lit in clause:
|
||||
lra.assert_lit(lit)
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == False
|
||||
assert sorted(lra.check()[1]) in [[-1, 2], [-2, 1]]
|
||||
|
||||
bf = ~Q.gt(x, 1) & ~Q.lt(x, 0)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for clause in enc.data:
|
||||
for lit in clause:
|
||||
lra.assert_lit(lit)
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == True
|
||||
|
||||
bf = ~Q.gt(x, 0) & ~Q.lt(x, 1)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for clause in enc.data:
|
||||
for lit in clause:
|
||||
lra.assert_lit(lit)
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == False
|
||||
|
||||
bf = ~Q.gt(x, 0) & ~Q.le(x, 0)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for clause in enc.data:
|
||||
for lit in clause:
|
||||
lra.assert_lit(lit)
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == False
|
||||
|
||||
bf = ~Q.le(x+y, 2) & ~Q.ge(x-y, 2) & ~Q.ge(y, 0)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for clause in enc.data:
|
||||
for lit in clause:
|
||||
lra.assert_lit(lit)
|
||||
assert len(lra.enc_to_boundary) == 3
|
||||
assert lra.check()[0] == False
|
||||
assert len(lra.check()[1]) == 3
|
||||
assert all(i > 0 for i in lra.check()[1])
|
||||
|
||||
|
||||
def test_unhandled_input():
|
||||
nan = S.NaN
|
||||
bf = Q.gt(3, nan) & Q.gt(x, nan)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
raises(ValueError, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
|
||||
|
||||
bf = Q.gt(3, I) & Q.gt(x, I)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
|
||||
|
||||
bf = Q.gt(3, float("inf")) & Q.gt(x, float("inf"))
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
|
||||
|
||||
bf = Q.gt(3, oo) & Q.gt(x, oo)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
|
||||
|
||||
# test non-linearity
|
||||
bf = Q.gt(x**2 + x, 2)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
|
||||
|
||||
bf = Q.gt(cos(x) + x, 2)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
|
||||
|
||||
@XFAIL
|
||||
def test_infinite_strict_inequalities():
|
||||
# Extensive testing of the interaction between strict inequalities
|
||||
# and constraints containing infinity is needed because
|
||||
# the paper's rule for strict inequalities don't work when
|
||||
# infinite numbers are allowed. Using the paper's rules you
|
||||
# can end up with situations where oo + delta > oo is considered
|
||||
# True when oo + delta should be equal to oo.
|
||||
# See https://math.stackexchange.com/questions/4757069/can-this-method-of-converting-strict-inequalities-to-equisatisfiable-nonstrict-i
|
||||
bf = (-x - y >= -float("inf")) & (x > 0) & (y >= float("inf"))
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for lit in sorted(enc.encoding.values()):
|
||||
if lra.assert_lit(lit) is not None:
|
||||
break
|
||||
assert len(lra.enc_to_boundary) == 3
|
||||
assert lra.check()[0] == True
|
||||
|
||||
|
||||
def test_pivot():
|
||||
for _ in range(10):
|
||||
m = randMatrix(5)
|
||||
rref = m.rref()
|
||||
for _ in range(5):
|
||||
i, j = randint(0, 4), randint(0, 4)
|
||||
if m[i, j] != 0:
|
||||
assert LRASolver._pivot(m, i, j).rref() == rref
|
||||
|
||||
|
||||
def test_reset_bounds():
|
||||
bf = Q.ge(x, 1) & Q.lt(x, 1)
|
||||
enc = boolean_formula_to_encoded_cnf(bf)
|
||||
lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
|
||||
for clause in enc.data:
|
||||
for lit in clause:
|
||||
lra.assert_lit(lit)
|
||||
assert len(lra.enc_to_boundary) == 2
|
||||
assert lra.check()[0] == False
|
||||
|
||||
lra.reset_bounds()
|
||||
assert lra.check()[0] == True
|
||||
for var in lra.all_var:
|
||||
assert var.upper == LRARational(float("inf"), 0)
|
||||
assert var.upper_from_eq == False
|
||||
assert var.upper_from_neg == False
|
||||
assert var.lower == LRARational(-float("inf"), 0)
|
||||
assert var.lower_from_eq == False
|
||||
assert var.lower_from_neg == False
|
||||
assert var.assign == LRARational(0, 0)
|
||||
assert var.var is not None
|
||||
assert var.col_idx is not None
|
||||
|
||||
|
||||
def test_empty_cnf():
|
||||
cnf = CNF()
|
||||
enc = EncodedCNF()
|
||||
enc.from_cnf(cnf)
|
||||
lra, conflict = LRASolver.from_encoded_cnf(enc)
|
||||
assert len(conflict) == 0
|
||||
assert lra.check() == (True, {})
|
||||
Reference in New Issue
Block a user