mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Merge pull request #8 from TheRealNebus/opt

Browse source 
Opt
This commit is contained in:
Nikolaj Bjorner 2017-10-27 12:49:12 -07:00 committed by GitHub
parent 0919fd4075 f1bad91609
commit 5989de1ae3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 7 additions and 7 deletions
Show stats 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):
"""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):
"""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):
"""Return an AST vector containing all added constraints.

8
src/sat/sat_simplifier.cpp
View file

@ -1037,7 +1037,7 @@ namespace sat {
block_clause(c, l, new_entry);
s.m_num_blocked_clauses++;
}
s.unmark_all(c);
s.unmark_all(c);
}
for (clause* c : m_to_remove)
s.block_clause(*c);
@ -1087,8 +1087,8 @@ namespace sat {
}
else {
unsigned j = 0;
for (literal lit : inter)
if (c.contains(lit))
for (literal lit : inter)
if (c.contains(lit))
inter[j++] = lit;
inter.shrink(j);
if (j == 0) return false;
@ -1344,7 +1344,7 @@ namespace sat {
clause_use_list & neg_occs = s.m_use_list.get(~l);
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();
if (c.is_blocked()) continue;
m_counter -= c.size();

2
src/sat/sat_simplifier_params.pyg
View file

@ -20,6 +20,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'),
('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_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.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))