mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-10-27 15:41:24 -07:00
commit 2a8a28bb59
3 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3/z3.py
View file

@ -6315,11 +6315,11 @@ class Solver(Z3PPObject):
def from_file(self, filename): def from_file(self, filename):
"""Parse assertions from a file""" """Parse assertions from a file"""
self.add([f for f in parse_smt2_file(filename)]) self.add([f for f in parse_smt2_file(filename, ctx=self.ctx)])
def from_string(self, s): def from_string(self, s):
"""Parse assertions from a string""" """Parse assertions from a string"""
self.add([f for f in parse_smt2_string(s)]) self.add([f for f in parse_smt2_string(s, ctx=self.ctx)])
def assertions(self): def assertions(self):
"""Return an AST vector containing all added constraints. """Return an AST vector containing all added constraints.

2
src/sat/sat_simplifier.cpp
View file

@ -1416,7 +1416,7 @@ namespace sat {
clause_use_list & neg_occs = s.m_use_list.get(~l); clause_use_list & neg_occs = s.m_use_list.get(~l);
clause_use_list::iterator it = neg_occs.mk_iterator(); clause_use_list::iterator it = neg_occs.mk_iterator();
for (; !it.at_end(); it.next()) { for (; !it.at_end(); it.next()) {
clause & c = it.curr(); clause & c = it.curr();
if (c.is_blocked()) continue; if (c.is_blocked()) continue;
m_counter -= c.size(); m_counter -= c.size();

2
src/sat/sat_simplifier_params.pyg
View file

@ -22,6 +22,6 @@ def_module_params(module_name='sat',
('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'), ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'), ('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'),
('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'), ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'), ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
('subsumption', BOOL, True, 'eliminate subsumed clauses'), ('subsumption', BOOL, True, 'eliminate subsumed clauses'),
('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)'))) ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))