check_context_with_model (issue)

[hudakhadiri]

Hello!
I'm currently using yices2_python_bindings to test a very simple example where I'm just trying to find a model that satisfies my constraints.

I'm using the function check_context_with_model, and I’ve already provided all the required configuration information for the context. However, I keep getting the following error:
"The function check_context_with_model failed because: operation not supported by the context"

I’ve tested both options for the params argument (params=None and params=Parameters()), but I still get the same error in both cases.
Here’s a minimal example of my code:

from yices import *

cfg = Config()
cfg.default_config_for_logic("QF_LRA")
cfg.set_config(key="solver-type", value="mcsat")
cfg.set_config(key="model-interpolation", value="true")
cfg.set_config(key="mode", value="multi-checks")
ctx = Context(cfg)

x = Terms.new_uninterpreted_term(Types.int_type(), "x")
a = Terms.new_uninterpreted_term(Types.int_type(), "a")
b = Terms.new_uninterpreted_term(Types.int_type(), "b")

x = a + b

x = Terms.add(a, b)

(a > 2) & (b > 2) & (x < 8) my constraints

constraints = [
Terms.arith_gt_atom(a, Terms.parse_float("2")),
Terms.arith_gt_atom(b, Terms.parse_float("2")),
Terms.arith_lt_atom(x, Terms.parse_float("8")),
]

ctx.assert_formulas(constraints)

model = Model()
model.set_integer(a, 3)

param = Parameters()

if ctx.check_context_with_model(params=None, model=model, python_array_or_tuple=[a, b]):
print("SAT")
else:
print("UNSAT")

Thank you so much in advance for your help!

[bobot]

We found our error. We used cfg.default_config_for_logic("QF_LRA"), the other set config are ignored or not sufficient to get back to a correct configuration for check_context_with_model.

[bobot]

Looking at the code of yices2 (decode_config), the difficulty is that once the logic is selected all the other options are ignored. Usually one can precise a default. Perhaps with the current semantic, it should be an error to set options after selecting the logic.