mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fixed bug in duality logging

Browse source
This commit is contained in:
Ken McMillan 2013-11-15 11:24:02 -08:00
parent 9cba5d7c85
commit 8320144af0
1 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/duality/duality_rpfp.cpp
View file

@ -89,15 +89,17 @@ namespace Duality {
if(memo.find(t) != memo.end())
return;
memo.insert(t);
decl_kind k = t.decl().get_decl_kind();
if(k == And || k == Or || k == Not || k == Implies || k == Iff){
ops++;
int nargs = t.num_args();
for(int i = 0; i < nargs; i++)
SummarizeRec(memo,lits,ops,t.arg(i));
if(t.is_app()){
decl_kind k = t.decl().get_decl_kind();
if(k == And || k == Or || k == Not || k == Implies || k == Iff){
ops++;
int nargs = t.num_args();
for(int i = 0; i < nargs; i++)
SummarizeRec(memo,lits,ops,t.arg(i));
return;
}
}
else
lits.push_back(t);
lits.push_back(t);
}
int Z3User::CumulativeDecisions(){