mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fixed problem with nullary background constants in duality

Browse source
This commit is contained in:
Ken McMillan 2013-06-10 14:46:15 -07:00
parent c21cd6ffa5
commit 30a4627a1e
2 changed files with 42 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/duality/duality.h
View file

@ -79,10 +79,6 @@ namespace Duality {
int CumulativeDecisions();
Term SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t);
Term SubstBound(hash_map<int,Term> &subst, const Term &t);
private:
void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
@ -162,6 +158,12 @@ namespace Duality {
bool weak = false
) = 0;
/** Declare a constant in the background theory. */
virtual void declare_constant(const func_decl &f) = 0;
/** Is this a background constant? */
virtual bool is_constant(const func_decl &f) = 0;
/** Assert a background axiom. */
virtual void assert_axiom(const expr &axiom) = 0;
@ -224,10 +226,24 @@ namespace Duality {
islvr->write_interpolation_problem(file_name,assumptions,theory);
#endif
}
/** Declare a constant in the background theory. */
virtual void declare_constant(const func_decl &f){
bckg.insert(f);
}
/** Is this a background constant? */
virtual bool is_constant(const func_decl &f){
return bckg.find(f) != bckg.end();
}
~iZ3LogicSolver(){
// delete ictx;
delete islvr;
}
private:
hash_set<func_decl> bckg;
};
#if 0
@ -478,6 +494,10 @@ namespace Duality {
void AssertNode(Node *n);
/** Declare a constant in the background theory. */
void DeclareConstant(const FuncDecl &f);
/** Assert a background axiom. Background axioms can be used to provide the
* theory of auxilliary functions or relations. All symbols appearing in
* background axioms are considered global, and may appear in both transformer
@ -771,6 +791,12 @@ namespace Duality {
void GetLabelsRec(hash_map<ast,int> &memo, const Term &f, std::vector<symbol> &labels,
hash_set<ast> *done, bool truth);
Term SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t);
Term SubstBound(hash_map<int,Term> &subst, const Term &t);
};
/** RPFP solver base class. */

16
src/duality/duality_rpfp.cpp
View file

@ -205,7 +205,7 @@ namespace Duality {
if(rit != e->relMap.end())
res = RedDualRela(e,args,(rit->second));
else {
if (args.size() == 0 && f.get_decl_kind() == Uninterpreted)
if (args.size() == 0 && f.get_decl_kind() == Uninterpreted && !ls->is_constant(f))
{
res = HideVariable(t,e->number);
}
@ -520,6 +520,12 @@ namespace Duality {
}
}
/** Declare a constant in the background theory. */
void RPFP::DeclareConstant(const FuncDecl &f){
ls->declare_constant(f);
}
/** Assert a background axiom. Background axioms can be used to provide the
* theory of auxilliary functions or relations. All symbols appearing in
* background axioms are considered global, and may appear in both transformer
@ -1828,7 +1834,7 @@ namespace Duality {
return RemoveLabelsRec(memo,t,lbls);
}
Z3User::Term Z3User::SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t)
RPFP::Term RPFP::SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t)
{
std::pair<ast,Term> foo(t,expr(ctx));
std::pair<hash_map<ast,Term>::iterator, bool> bar = memo[level].insert(foo);
@ -1839,6 +1845,8 @@ namespace Duality {
func_decl f = t.decl();
std::vector<Term> args;
int nargs = t.num_args();
if(nargs == 0)
ls->declare_constant(f); // keep track of background constants
for(int i = 0; i < nargs; i++)
args.push_back(SubstBoundRec(memo, subst, level, t.arg(i)));
res = f(args.size(),&args[0]);
@ -1858,7 +1866,7 @@ namespace Duality {
return res;
}
Z3User::Term Z3User::SubstBound(hash_map<int,Term> &subst, const Term &t){
RPFP::Term RPFP::SubstBound(hash_map<int,Term> &subst, const Term &t){
hash_map<int,hash_map<ast,Term> > memo;
return SubstBoundRec(memo, subst, 0, t);
}
@ -2037,7 +2045,7 @@ namespace Duality {
int nargs = t.num_args();
for(int i = 0; i < nargs; i++)
WriteEdgeVars(e, memo, t.arg(i),s);
if (nargs == 0 && f.get_decl_kind() == Uninterpreted){
if (nargs == 0 && f.get_decl_kind() == Uninterpreted && !ls->is_constant(f)){
Term rename = HideVariable(t,e->number);
Term value = dualModel.eval(rename);
s << " (= " << t << " " << value << ")\n";