mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fixed bug in label output in duality

Browse source
This commit is contained in:
Ken McMillan 2013-05-09 14:24:22 -07:00
parent dc793907a5
commit 477754c386
3 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/duality/duality.h
View file

@ -672,6 +672,8 @@ namespace Duality {
TermTree *GetGoalTree(Node *root); TermTree *GetGoalTree(Node *root);
int EvalTruth(hash_map<ast,int> &memo, Edge *e, const Term &f);
private: private:
@ -733,10 +735,8 @@ namespace Duality {
Term ProjectFormula(std::vector<Term> &keep_vec, const Term &f); Term ProjectFormula(std::vector<Term> &keep_vec, const Term &f);
public:
int SubtermTruth(hash_map<ast,int> &memo, const Term &); int SubtermTruth(hash_map<ast,int> &memo, const Term &);
private:
void ImplicantRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits, void ImplicantRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
hash_set<ast> *done, bool truth, hash_set<ast> &dont_cares); hash_set<ast> *done, bool truth, hash_set<ast> &dont_cares);

4
src/duality/duality_rpfp.cpp
View file

@ -833,6 +833,10 @@ namespace Duality {
return res; return res;
} }
int RPFP::EvalTruth(hash_map<ast,int> &memo, Edge *e, const Term &f){
Term tl = Localize(e, f);
return SubtermTruth(memo,tl);
}
#ifdef Z3OPS #ifdef Z3OPS
static Z3_subterm_truth *stt; static Z3_subterm_truth *stt;

2
src/muz_qe/duality_dl_interface.cpp
View file

@ -270,7 +270,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
hash_map<ast,int> memo; hash_map<ast,int> memo;
for(unsigned j = 0; j < labels.size(); j++){ for(unsigned j = 0; j < labels.size(); j++){
RPFP::label_struct &lab = labels[j]; RPFP::label_struct &lab = labels[j];
int truth = cex.tree->SubtermTruth(memo,lab.value); int truth = cex.tree->EvalTruth(memo,&edge,lab.value);
if(truth == 1 && lab.pos || truth == 0 && !lab.pos) if(truth == 1 && lab.pos || truth == 0 && !lab.pos)
out << " " << lab.name; out << " " << lab.name;
} }