Use solver_options to specify solver-dependent options #338

marcogario · 2016-10-04T09:31:01Z

Options that are shared by multiple solvers are handled as keywords
arguments, but solver-dependent options are defined in the
solver_options dictionary:

Solver(name='picosat', generate_models=True,
solver_options={'propagation_limit': 100})

The goal is to clearly separate these two type of configurations.
The use of dictionary for solver_options, makes it simple to store
multiple configurations:

Solver(name=sname, solver_options=myoptions[sname])

All solvers have been ported to this new strategy, by using a custom
SolverOptions object that is responsible for the definition, checking
and setting of the options. This object is used (for example) to
correctly setup the mathsat context.

Option "random_seed" is now supported by all the solvers (that do
support it).

Backwards Incompatible Changes:

MathSAT5Solver option 'debugFile' has been removed. Use the
solver option: "debug_api_call_trace_filename".
BddSolver used to have the options as keyword
arguments (static_ordering, dynamic_reordering etc). This is not
supported anymore.

Options that are shared by multiple solvers are handled as keywords arguments, but solver-dependent options are defined in the solver_options dictionary: Solver(name='picosat', generate_models=True, solver_options={'propagation_limit': 100}) The goal is to clearly separate these two type of configurations. The use of dictionary for solver_options, makes it simple to store multiple configurations: Solver(name=sname, solver_options=myoptions[sname]) All solvers have been ported to this new strategy, by using a custom SolverOptions object that is responsible for the definition, checking and setting of the options. This object is used (for example) to correctly setup the mathsat context. Option "random_seed" is now supported by all the solvers (that do support it). Deprecation: Backwards Incompatible Changes: * MathSAT5Solver option 'debugFile' has been removed deprecated. Use the solver option: "debug_api_call_trace_filename". * BddSolver used to have the options as keyword arguments (static_ordering, dynamic_reordering etc). This is not supported anymore.

CVC4 configure using the default path of the 'python' executable to compile the python bindings. On systems where multiple versions of python are installed, running install.py with a different version of python (e.g., python3.5) would lead to the creation of invalid bindings.

CVC4.OptionException is not a valid python 3 exception (since it does not inherit from BaseException). Therefore, in python 3, we cannot use a regular try/except to catch it. This should be fixed in the CVC4 wrapper, here we simply work around the issue.

This also upgrade to the latest wrapper

marcogario · 2016-10-04T09:32:51Z

This PR includes two additional changes:

CVC4 installer is more robust when installing on a system with multiple version of python
pyPicosat has been extended to better deal with flushing of the output log.

mikand

The PR looks great and solves the option issue in a very clean way. I marked few points to fix/discuss before accepting.

mikand · 2016-10-07T11:31:47Z

pysmt/smtlib/solver.py

+            solver.set_option(":random-seed", str(self.random_seed))
+
+        for k,v in self.solver_options.items():
+            if k in (':print-success', 'diagnostic-output-channel'):


What if the user pusts :produce-models in the solver_options? Maybe we should avoid overriding all the pysmt-interpreted options.

Not sure if I understand this point.

mikand · 2016-10-07T11:33:30Z

pysmt/smtlib/solver.py

@@ -86,13 +123,13 @@ def _send_silent_command(self, cmd):
    def _get_answer(self):
        """Reads a line from STDOUT pipe"""
        res = self.solver_stdout.readline().strip()
-        if self.dbg: print("Read: " + str(res))
+        if self.options.debug_interaction: print("Read: " + str(res))


You could use _debug

mikand · 2016-10-07T11:35:34Z

pysmt/smtlib/solver.py

@@ -71,9 +104,13 @@ def set_option(self, name, value):
    def set_logic(self, logic):
        self._send_silent_command(SmtLibCommand(smtcmd.SET_LOGIC, [logic]))

+    def _debug(self, msg):


To save a little bit of time you could change _debug as follows.

def _debug(self, msg, *format_args): if self.options.debug_interaction: print(msg % format_args)

In this way, we can avoid the construction of the debug string if the debugging is not enabled.

mikand · 2016-10-07T11:35:57Z

pysmt/smtlib/solver.py

        return res

    def _get_value_answer(self):
        """Reads and parses an assignment from the STDOUT pipe"""
        lst = self.parser.get_assignment_list(self.solver_stdout)
-        if self.dbg: print("Read: " + str(lst))
+        if self.options.debug_interaction: print("Read: " + str(lst))


You should use _debug

mikand · 2016-10-07T11:44:36Z

pysmt/solvers/cvc4.py

+
+    def __init__(self, **base_options):
+        SolverOptions.__init__(self, **base_options)
+        # TODO: CVC4 Supports UnsatCore extraction


Add reference to #349

mikand · 2016-10-07T11:45:04Z

pysmt/solvers/cvc4.py

@@ -98,7 +125,7 @@ def solve(self, assumptions=None):
        else:
            try:
                res = self.cvc4.checkSat()
-            except CVC4.LogicException as ex:
+            except:
                raise InternalSolverError(ex.toString())


ex variable is now unassigned!

mikand · 2016-10-07T11:54:14Z

pysmt/solvers/yices.py

+class YicesOptions(SolverOptions):
+    def __init__(self, **base_options):
+        SolverOptions.__init__(self, **base_options)
+        # TODO: Yices Supports UnsatCore extraction


AFAIK Yices does NOT support Unsat Core extraction

You are right. The manual explicitly says so.

mikand · 2016-10-07T11:56:49Z

pysmt/solvers/yices.py

        self.converter = YicesConverter(environment)
        self.mgr = environment.formula_manager
        self.model = None
        self.failed_pushes = 0
        return

+    def _create_yices_context(self):


Why is this in a separate method? All the other solvers have this in their constructor, and this method is only called from there....

Mostly because there is a bit of additional code to handle 1) the logic selection 2) setting of parameters (set_params) 3) freeing of configuration.

We can also probably just isolate the bit about the logic conversion.

mikand · 2016-10-07T11:59:01Z

pysmt/test/test_rewritings.py

@@ -15,6 +15,7 @@
 #   See the License for the specific language governing permissions and
 #   limitations under the License.
 #
+from nose.plugins.attrib import attr


Is this used?

coveralls · 2016-10-07T12:50:51Z

Changes Unknown when pulling b45cb35 on i105/options into * on master*.

coveralls · 2016-10-07T12:50:51Z

Changes Unknown when pulling b45cb35 on i105/options into * on master*.

Use solver_options to specify solver-dependent options

marcogario added 5 commits October 4, 2016 11:29

Tests: Remove TimesDistributor NIA tests

b609e6d

pyPicosat: Force flush of output file

b4ac32b

This also upgrade to the latest wrapper

marcogario added the enhancement label Oct 4, 2016

marcogario added this to the 0.6.0 milestone Oct 4, 2016

marcogario assigned mikand Oct 4, 2016

This was referenced Oct 4, 2016

CVC4: Use on python-config in ./configure #336

Closed

Pasing options to Solvers / QuantifierEliminators / Interpolator #105

Closed

CVC4: Conditionally use PYTHON_CONFIG

26b700b

mikand requested changes Oct 7, 2016

View reviewed changes

marcogario added 2 commits October 7, 2016 14:21

SMTLIB: Test handling of 'debug_interaction'

b45cb35

Address PR comments

ffe75f7

mikand assigned marcogario and unassigned mikand Oct 7, 2016

Yices: Simplify context construction

843248b

marcogario mentioned this pull request Oct 7, 2016

Improve Yices usage #281

Open

marcogario assigned mikand and unassigned marcogario Oct 7, 2016

mikand approved these changes Oct 8, 2016

View reviewed changes

mikand merged commit 1fc9428 into master Oct 8, 2016

mikand deleted the i105/options branch October 8, 2016 12:31

nbailluet pushed a commit to nbailluet/pysmt that referenced this pull request Mar 14, 2024

Merge pull request pysmt#338 from pysmt/i105/options

aad203a

Use solver_options to specify solver-dependent options

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use solver_options to specify solver-dependent options #338

Use solver_options to specify solver-dependent options #338

marcogario commented Oct 4, 2016

marcogario commented Oct 4, 2016

mikand left a comment

mikand Oct 7, 2016

marcogario Oct 7, 2016

mikand Oct 7, 2016

mikand Oct 7, 2016

mikand Oct 7, 2016 •

edited

mikand Oct 7, 2016

mikand Oct 7, 2016 •

edited

mikand Oct 7, 2016

marcogario Oct 7, 2016

mikand Oct 7, 2016

marcogario Oct 7, 2016

mikand Oct 7, 2016

coveralls commented Oct 7, 2016 •

edited

coveralls commented Oct 7, 2016

Use solver_options to specify solver-dependent options #338

Use solver_options to specify solver-dependent options #338

Conversation

marcogario commented Oct 4, 2016

marcogario commented Oct 4, 2016

mikand left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mikand Oct 7, 2016 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mikand Oct 7, 2016 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

coveralls commented Oct 7, 2016 • edited

coveralls commented Oct 7, 2016

mikand Oct 7, 2016 •

edited

mikand Oct 7, 2016 •

edited

coveralls commented Oct 7, 2016 •

edited