Commit 2851903d authored by Fabrizio Detassis's avatar Fabrizio Detassis
Browse files

WIP - smt

parent 7a892284
......@@ -13,13 +13,24 @@ import threading
import sys
import multiprocess
import multiprocessing
import time
from pebble import concurrent
from concurrent.futures import TimeoutError
class TimeoutException(Exception):
pass
@concurrent.process(timeout=5, context=multiprocessing.get_context('spawn')) # You can adjust the timeout here
def solve(formula):
with Solver(name='msat') as s:
s.add_assertion(formula)
return s.solve()
@contextmanager
def time_limit(seconds, msg=''):
timer = threading.Timer(seconds, lambda: _thread.interrupt_main())
......@@ -57,6 +68,66 @@ class SMTModel:
domain = self.domain
loss = self.loss
ub = None
lb = None
print("Optimizing SMT Model")
unsat_counts = 0
if is_sat(domain, solver_name='msat'):
while it < max_iter and unsat_counts < 3:
print("Iteration ", str(it))
# print(solver.print_model())
if ub is None:
print("Retrieving the initial solution value")
# ub = solver.get_py_value(loss)
ub = 1.0
if lb is None:
lb = 0
print("Bounds: [%.2f - %.2f]" % (lb, ub))
if np.abs(ub - lb) > 0.01:
it += 1
else:
break
bound = (ub + lb) / 2
s = solve(And(domain, LT(loss, Real(bound))))
sat = s.result()
print(sat)
# Update the bounds.
if sat:
ub = bound
unsat_counts = 0
print("SAT!")
else:
print("UNSAT!")
lb = bound
unsat_counts += 1
print("Retrieving the solution value")
# Distinguish between regression and classification models.
with Solver('msat') as solver:
if isinstance(self.variables[0], list):
y_opt = [
[float(solver.get_py_value(_y)) for _y in y] for y in self.variables
]
else:
y_opt = [float(solver.get_py_value(y)) for y in self.variables]
return y_opt
else:
print("Problem not satisfiable!")
def optimize_OLD1(self, max_iter=20):
it = 0
domain = self.domain
loss = self.loss
ub = None
lb = None
print("Optimizing SMT Model")
......@@ -70,7 +141,9 @@ class SMTModel:
print("Iteration ", str(it))
# print(solver.print_model())
if ub is None:
ub = solver.get_py_value(loss)
print("Retrieving the initial solution value")
# ub = solver.get_py_value(loss)
ub = 1.0
if lb is None:
lb = 0
......@@ -85,6 +158,7 @@ class SMTModel:
solver.add_assertion(LT(loss, Real(bound)))
solver.push()
"""
try:
with time_limit(self._TIME_LIMIT):
sat = solver.solve()
......@@ -92,7 +166,7 @@ class SMTModel:
except TimeoutException:
print("Timed out!")
sat = False
"""
"""
sat = False
......@@ -105,8 +179,9 @@ class SMTModel:
if p.is_alive():
print("Timed out!")
p.terminate()
"""
p.close()
"""
manager = multiprocess.Manager()
return_dict = manager.dict()
p = multiprocess.Process(target=self.solve, args=(solver, return_dict))
......@@ -118,22 +193,49 @@ class SMTModel:
p.terminate()
sat = return_dict['sat']
if sat is None:
sat = False
"""
"""
pool = multiprocess.Pool(1)
kwargs = {"formula": domain, "solver_name": "msat"}
future_res_sat = pool.apply_async(is_sat, kwds=kwargs)
# future_res_sat = pool.apply_async(time.sleep, (15,))
sat = future_res_sat.get(10)
print("sat", sat)
"""
"""
kwargs = {"formula": domain, "solver_name": "msat"}
with threading.Thread(target=is_sat, kwargs=kwargs) as t:
t.start()
t.join(self._TIME_LIMIT)
if t.is_alive():
t.terminate()
sat = False
print("Time Limit reached")
future_res_sat = pool.apply_async()
sat = future_res_sat.get(10)
print("sat", sat)
"""
@concurrent.process(timeout=self._TIME_LIMIT, context=multiprocessing)
def solve():
return solver.solve()
s = solve()
sat = s.result()
print(sat)
sat2 = solver.solve()
print("sat2", sat2)
# Update the bounds.
if sat:
ub = bound
# Distinguish between regression and classification models.
if isinstance(self.variables[0], list):
y_opt = [
[float(solver.get_py_value(_y)) for _y in y] for y in self.variables
]
else:
y_opt = [float(solver.get_py_value(y)) for y in self.variables]
unsat_counts = 0
print("SAT!")
......@@ -143,13 +245,23 @@ class SMTModel:
lb = bound
unsat_counts += 1
print("Retrieving the solution value")
# Distinguish between regression and classification models.
if isinstance(self.variables[0], list):
y_opt = [
[float(solver.get_py_value(_y)) for _y in y] for y in self.variables
]
else:
y_opt = [float(solver.get_py_value(y)) for y in self.variables]
return y_opt
else:
print("Problem not satisfiable!")
@staticmethod
def solve(solver, q):
def solve_OLD(solver, q):
sat = solver.solve()
q.put(sat)
# q['sat'] = sat
......@@ -540,3 +652,193 @@ class MovingTargetClsSMT(MovingTarget):
# print("Variables added: " + str(self.variables))
return mod
if __name__ == '__main__':
from abc import ABC, abstractmethod
from aiddl_core.representation.symbolic import Symbolic
from aiddl_core.representation.integer import Integer
from aiddl_core.representation.infinity import Infinity
from aiddl_core.representation.tuple import Tuple
from aiddl_core.container.container import Container
import aiddl_core.function.default as dfun
from aiddl_core.tools.logger import Logger
from aiddl_core.parser.parser import parse_term
import aiddl_core.parser.parser as parser
from aiddl_network.grpc_function import GrpcFunction
from aiddl_network.aiddl_grpc_server import AiddlServicer
from aiddl_network.aiddl_grpc_server import LOADER_URI
# from moving_target_cplex import MovingTargetRegCplex, MovingTargetClsCplex
# from moving_target_smt import MovingTargetRegSMT
from factory import get_problem
from tools import CsvLoader
from scikit_learn_wrapper import SciKitLearnFunction
# Loaded modules (aka AIDDL files) go to container:
C = Container()
# Loaded functions (#def in modules, or MovingTargetCplex instance)
# go to function registry:
F = dfun.get_default_function_registry(C)
# Load example (returns URI of module)
# example_module_uri = parser.parse("../../aiddl/example-01.aiddl", C, F)
# example_module_uri = parser.parse("../../aiddl/example-fair-reg.aiddl", C, F)
loader = CsvLoader()
adult_example_module_uri = loader.apply(parse_term('("../../resources/adult_reduced.csv" "," "income")'))
crime_example_module_uri = loader.apply(parse_term('("../../resources/crime_train.csv" "," "violentPerPop")'))
# Fetch "examples" entry from module:
# example_entry = C.get_entry(Symbolic("examples"), module=example_module_uri)
# Take value of entry:
# example_data = example_entry.get_value()
adult_mt_cfg = parse_term('''(
n:3 ;; Number of iterations
alpha:1 ;; Parameter alpha
beta:1 ;; Parameter beta
problem-type:classification ;; classification/regression?
constraint-solver:smt ;; Select constraint solver (cplex/pysmt)
learner:mt.learner ;; URI of learner (registered above)
)''')
adult_mt_data = parse_term('''{
loss-function:HammingDistance ;; Select loss function
constraints:{
(didi-bin "income" ["race_Amer-Indian-Eskimo" "race_Asian-Pac-Islander" "race_Black" "race_Other" "race_White"] 0.2)
}
}''')
crime_mt_cfg = parse_term('''(
n:3 ;; Number of iterations
alpha:1 ;; Parameter alpha
beta:1 ;; Parameter beta
problem-type:regression ;; classification/regression?
constraint-solver:cplex ;; Select constraint solver (cplex/pysmt)
learner:mt.learner ;; URI of learner (registered above)
)''')
crime_mt_data = parse_term('''{
loss-function:MeanAbsoluteError ;; Select loss function
constraints:{
(didi-real "violentPerPop" ["race"] 0.01)
}
}''')
mt_data = adult_mt_data.put_all(adult_example_module_uri)
# NOTE: The following part relies on org.aiddl.network which I still need to publish...
# Connection to AIDDL GrpcServer
host = "localhost"
port = 8011
# Create function that can create functions on server
f_create = GrpcFunction(host,
port,
Symbolic("org.aiddl.eval.load-function"))
# Data neeed to create learner through f_create
dt_learner_conf = parser.parse_term('''
(
name:ID3
module:my
class:org.aiddl.common.learning.decision_tree.ID3
config:{}
)
''')
ls_expansion = parser.parse_term('''
(
name:Expansion
module:my
class:org.aiddl.common.learning.linear_regression.ExpansionFunction
config:{}
)
''')
f_create.apply(ls_expansion)
ls_learner_conf = parser.parse_term('''
(
name:LeastSquares
module:my
class:org.aiddl.common.learning.linear_regression.LinearRegression
config:{ expansion:^my.Expansion }
)
''')
lap_cfg = parser.parse_term('''
(
name:LearnAndApplyFunction
module:my
class:org.aiddl.common.learning.supervised.LearnAndApplyFunction
config:{ learner:^my.LeastSquares }
)
''')
# Create function on server
dt_learner_uri = f_create.apply(dt_learner_conf)
# Create local proxy to newly created function
f_ID3 = GrpcFunction(host, port, dt_learner_uri)
# Create function on server
mse_learner_uri = f_create.apply(ls_learner_conf)
# Create local proxy to newly created function
f_MSE = GrpcFunction(host, port, mse_learner_uri)
# Create function on server
lap_uri = f_create.apply(lap_cfg)
# Create local proxy to newly created function
f_LAP = GrpcFunction(host, port, lap_uri)
# Finally, we can apply mean square error to data:
# weights = f_MSE.apply(example_data)
# print("Weights:", weights)
# y_k = f_LAP.apply(example_data)
# print("Result:", y_k)
# Create local function to expand data and
# hook it into least squares function running on server
# class ExpandData:
# def apply(self, x):
# return Tuple([Integer(1), x])
# F.add_function(ExpandData(), Symbolic("my.expander"))
# mt_data = C.get_entry(Symbolic("moving-targets-problem"), module=example_module_uri).get_value()
# mt_data = mt_data.resolve(C)
# mtc = MovingTargetRegCplex(f_LAP, n=30)
# mtc = MovingTargetClsCplex(f_LAP, n=10)
# mtc = MovingTargetRegSMT(f_LAP, n=5)
learner = parse_term('''{
py_module:sklearn.ensemble
py_class:RandomForestClassifier
n_estimators:50
max_depth:5
}''')
f_ML = SciKitLearnFunction(learner)
F.add_function(Symbolic("mt.learner"), f_ML)
# Take value of entry:
problem_type = adult_mt_cfg[Symbolic("problem-type")].string_value()
solver_type = adult_mt_cfg[Symbolic("constraint-solver")].string_value()
movt_class = get_problem(problem_type, solver=solver_type)
mtc = movt_class(adult_mt_cfg, F)
# print(Logger.pretty_print(mt_data, 0))
mtc.apply(mt_data)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment