Skip to content

Adts marshalling #15

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
BritikovKI wants to merge 5 commits into
base: Refactoring
Choose a base branch
from
Draft

Adts marshalling #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
3c761b4
ADT fix: found the issue and initial ideas on how to fix it
BritikovKI Jan 31, 2025
e2e821b
ADT fix: fixes on the go
Feb 2, 2025
cf05ecb
ADT fix: TODO rework fParser and SMTUtils so they have same ctx and z…
BritikovKI Feb 3, 2025
c60b2e0
ADT fix: working version of testgen with datatypes
Feb 3, 2025
599f066
ADT fix: cleaning up marshalling
BritikovKI Feb 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions include/ae/AeValSolver.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ namespace ufo
efac(s->getFactory()),
z3(efac),
smt (z3),
u(efac),
u(efac,z3),
fresh_var_ind(0),
partitioning_size(0),
debug(0)
Expand Down Expand Up @@ -794,7 +794,8 @@ namespace ufo
template<typename Range> static Expr eliminateQuantifiersRepl(Expr fla, Range& vars)
{
ExprFactory &efac = fla->getFactory();
SMTUtils u(efac);
EZ3 ez3(efac);
SMTUtils u(efac, ez3);
ExprSet complex;
findComplexNumerics(fla, complex);
ExprMap repls;
Expand Down Expand Up @@ -831,7 +832,8 @@ namespace ufo
inline static Expr abduce (Expr goal, Expr assm)
{
ExprFactory &efac = goal->getFactory();
SMTUtils u(efac);
EZ3 ez3(efac);
SMTUtils u(efac, ez3);
ExprSet complex;
findComplexNumerics(assm, complex);
findComplexNumerics(goal, complex);
Expand Down
22 changes: 10 additions & 12 deletions include/ae/SMTUtils.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ namespace ufo
private:

ExprFactory &efac;
EZ3 z3;
EZ3& z3;
ZSolver<EZ3> smt;
bool can_get_model;
ZSolver<EZ3>::Model* m;
Expand All @@ -24,14 +24,15 @@ namespace ufo

public:

SMTUtils (ExprFactory& _efac) :
efac(_efac), z3(efac), smt (z3), can_get_model(0), m(NULL) {}

SMTUtils (ExprFactory& _efac, unsigned _to) :
efac(_efac), z3(efac), smt (z3, _to), can_get_model(0), m(NULL) {}
SMTUtils (ExprFactory& _efac, EZ3& _z3) :
efac(_efac), z3(_z3), smt (z3), can_get_model(0), m(NULL) {}

SMTUtils (ExprFactory& _efac, ExprVector& _accessors, unsigned _to, bool _bv) :
efac(_efac), z3(efac), smt (z3, _to), can_get_model(0), m(NULL)
SMTUtils (ExprFactory& _efac, EZ3& _z3, unsigned _to) :
efac(_efac), z3(_z3), smt (z3, _to), can_get_model(0), m(NULL) {}

SMTUtils (ExprFactory& _efac, EZ3& _z3, ExprVector& _accessors, unsigned _to, bool _bv) :
efac(_efac), z3(_z3), smt (z3, _to), can_get_model(0), m(NULL)
{
approxBV = _bv;
for(auto b : _accessors)
Expand All @@ -42,12 +43,9 @@ namespace ufo
;
}

SMTUtils (ExprFactory& _efac, ExprVector& _accessors, unsigned _to, std::vector<Expr> adts, std::vector<std::string> adts_seen) :
efac(_efac), z3(efac), smt (z3, _to), can_get_model(0), m(NULL)
SMTUtils (ExprFactory& _efac, EZ3& _z3, ExprVector& _accessors, unsigned _to) :
efac(_efac), z3(_z3), smt (z3, _to), can_get_model(0), m(NULL)
{

z3.adts = adts;
z3.adts_seen = adts_seen;
for(auto b : _accessors)
if (b->arity() == 3)
accessors.insert(b);
Expand Down
2 changes: 1 addition & 1 deletion include/deep/NonlinCHCsolver.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ namespace ufo

NonlinCHCsolver(CHCs &r, map<string, map<string,vector<string>>> & s) :
m_efac(r.m_efac), ruleManager(r),
u(m_efac, r.m_z3.getAdtAccessors(), 10000, r.m_z3.adts, r.m_z3.adts_seen), signature(s) {}
u(m_efac, r.m_z3, r.m_z3.getAdtAccessors(), 10000), signature(s) {}

bool checkAllOver(bool checkQuery = false) {
for (auto &hr: ruleManager.chcs) {
Expand Down
8 changes: 2 additions & 6 deletions include/ufo/Smt/Z3n.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -283,9 +283,6 @@ namespace ufo
Z3_set_ast_print_mode (ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
}

public:
std::vector<Expr> adts;
std::vector<std::string> adts_seen;

protected:
z3::context &get_ctx () { return ctx; }
Expand All @@ -294,14 +291,14 @@ namespace ufo
expr_ast_map seen_expr;
z3::ast toAst (Expr e)
{
return M::marshal (e, get_ctx (), cache.left, seen_expr, adts, adts_seen);
return M::marshal (e, get_ctx (), cache.left, seen_expr);
}
Expr toExpr (z3::ast a)
{
if (!a) return Expr();

// ast_expr_map seen;
auto res = U::unmarshal (a, get_efac (), cache.right, seen_ast, adts_seen, adts, accessors);
auto res = U::unmarshal (a, get_efac (), cache.right, seen_ast, accessors);
return res;
}

Expand Down Expand Up @@ -352,7 +349,6 @@ namespace ufo
return out.str ();
}

ExprVector& getAdtConstructors(){ return adts; }
ExprVector& getAdtAccessors(){ return accessors; }

template <typename Range>
Expand Down
Loading