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

nits

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-25 10:40:08 -07:00
parent 168b0bcc44
commit 892be69d51
2 changed files with 9 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_special_relations.cpp
View file

@ -115,15 +115,11 @@ namespace smt {
void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) { void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) {
context& ctx = get_context(); context& ctx = get_context();
app_ref eq(get_manager());
app* t1 = get_enode(v1)->get_owner(); app* t1 = get_enode(v1)->get_owner();
app* t2 = get_enode(v2)->get_owner(); app* t2 = get_enode(v2)->get_owner();
eq = get_manager().mk_eq(t1, t2); literal eq = mk_eq(t1, t2, false);
VERIFY(internalize_atom(eq, false)); for (auto const& kv : m_relations) {
literal l(ctx.get_literal(eq)); relation& r = *kv.m_value;
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
for (; !ctx.inconsistent() && it != end; ++it) {
relation& r = *it->m_value;
if (!r.new_eq_eh(l, v1, v2)) { if (!r.new_eq_eh(l, v1, v2)) {
set_neg_cycle_conflict(r); set_neg_cycle_conflict(r);
break; break;
@ -175,9 +171,8 @@ namespace smt {
literal theory_special_relations::mk_literal(expr* _e) { literal theory_special_relations::mk_literal(expr* _e) {
expr_ref e(_e, get_manager()); expr_ref e(_e, get_manager());
context& ctx = get_context();
ensure_enode(e); ensure_enode(e);
return ctx.get_literal(e); return get_context().get_literal(e);
} }
theory_var theory_special_relations::mk_var(enode* n) { theory_var theory_special_relations::mk_var(enode* n) {
@ -520,7 +515,6 @@ namespace smt {
} }
expr_ref theory_special_relations::mk_inj(relation& r, model_generator& mg) { expr_ref theory_special_relations::mk_inj(relation& r, model_generator& mg) {
// context& ctx = get_context();
ast_manager& m = get_manager(); ast_manager& m = get_manager();
r.push(); r.push();
ensure_strict(r.m_graph); ensure_strict(r.m_graph);
@ -545,7 +539,6 @@ namespace smt {
} }
expr_ref theory_special_relations::mk_class(relation& r, model_generator& mg) { expr_ref theory_special_relations::mk_class(relation& r, model_generator& mg) {
//context& ctx = get_context();
ast_manager& m = get_manager(); ast_manager& m = get_manager();
expr_ref result(m); expr_ref result(m);
func_decl_ref fn(m); func_decl_ref fn(m);

10
src/smt/theory_special_relations.h
View file

@ -17,14 +17,14 @@ Notes:
--*/ --*/
#ifndef THEORY_SPECIAL_RELATIONS_H_
#define THEORY_SPECIAL_RELATIONS_H_
#include "ast/special_relations_decl_plugin.h" #include "ast/special_relations_decl_plugin.h"
#include "smt/smt_theory.h" #include "smt/smt_theory.h"
#include "smt/theory_diff_logic.h" #include "smt/theory_diff_logic.h"
#include "util/union_find.h" #include "util/union_find.h"
#include "solver/solver.h" #include "util/rational.h"
#ifndef THEORY_SPECIAL_RELATIONS_H_
#define THEORY_SPECIAL_RELATIONS_H_
namespace smt { namespace smt {
class theory_special_relations : public theory { class theory_special_relations : public theory {
@ -140,7 +140,7 @@ namespace smt {
void set_neg_cycle_conflict(relation& r); void set_neg_cycle_conflict(relation& r);
void set_conflict(relation& r); void set_conflict(relation& r);
lbool propagate_plo(atom& a); lbool propagate_plo(atom& a);
lbool propagate_po(atom& a); //ASHU: added to modify po solving lbool propagate_po(atom& a);
theory_var mk_var(expr* e); theory_var mk_var(expr* e);
void count_children(graph const& g, unsigned_vector& num_children); void count_children(graph const& g, unsigned_vector& num_children);
void ensure_strict(graph& g); void ensure_strict(graph& g);