mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

working on horn difference logic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-21 18:17:49 -07:00
parent 17f0377c06
commit 0fbdd37e89
13 changed files with 105 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_diff_logic_def.h
View file

@ -318,7 +318,7 @@ template<typename Ext>
void theory_diff_logic<Ext>::assign_eh(bool_var v, bool is_true) {
m_stats.m_num_assertions++;
atom * a = 0;
m_bool_var2atom.find(v, a);
VERIFY (m_bool_var2atom.find(v, a));
SASSERT(a);
SASSERT(get_context().get_assignment(v) != l_undef);
SASSERT((get_context().get_assignment(v) == l_true) == is_true);
@ -376,13 +376,6 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
SASSERT(is_consistent());
#if 0
TBD:
if (propagate_cheap_equalities()) {
return FC_CONTINUE;
}
#endif
if (m_non_diff_logic_exprs) {
return FC_GIVEUP;
}