Commit 0ba80e38 authored by Martin Jonas's avatar Martin Jonas
Browse files

Multiple changes

parent 4679128e
......@@ -9,9 +9,11 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
map<string, int> varCounts;
auto item = subformulaVariableCounts.find((Z3_ast)e);
if (item != subformulaVariableCounts.end() && (item->second).second == boundVars)
if (item != subformulaVariableCounts.end() && (subformulaMaxDeBruijnIndices[(Z3_ast)e] == -1 || (item->second).second == boundVars))
{
return {(item->second).first, subformulaMaxDeBruijnIndices[(Z3_ast)e]};
//probably can be return {varCounts, subformulaMaxDeBruijnIndices[(Z3_ast)e]};
//return {(item->second).first, subformulaMaxDeBruijnIndices[(Z3_ast)e]};
return {varCounts, subformulaMaxDeBruijnIndices[(Z3_ast)e]};
}
if (e.is_var())
......@@ -878,3 +880,54 @@ int UnconstrainedVariableSimplifier::getNumberOfLeadingZeroes(const z3::expr &e)
}
}
expr UnconstrainedVariableSimplifier::CanonizeBoundVariables(const expr &e)
{
if (e.is_app())
{
func_decl dec = e.decl();
int numArgs = e.num_args();
expr_vector arguments(e.ctx());
for (int i = 0; i < numArgs; i++)
{
arguments.push_back(CanonizeBoundVariables(e.arg(i)));
}
expr result = dec(arguments);
return result;
}
else if (e.is_quantifier())
{
Z3_ast ast = (Z3_ast)e;
int numBound = Z3_get_quantifier_num_bound(e.ctx(), ast);
Z3_sort sorts [numBound];
Z3_symbol decl_names [numBound];
for (int i = 0; i < numBound; i++)
{
sorts[i] = Z3_get_quantifier_bound_sort(e.ctx(), ast, i);
decl_names[i] = Z3_mk_string_symbol(e.ctx(), std::to_string(lastBound).c_str());
lastBound++;
}
Z3_ast quantAst = Z3_mk_quantifier(
e.ctx(),
Z3_is_quantifier_forall(e.ctx(), ast),
Z3_get_quantifier_weight(e.ctx(), ast),
0,
{},
numBound,
sorts,
decl_names,
(Z3_ast)CanonizeBoundVariables(e.body() && e.ctx().bool_val(true)));
auto result = to_expr(e.ctx(), quantAst);
return result;
}
else
{
return e;
}
}
This diff is collapsed.
......@@ -45,6 +45,7 @@ public:
z3::expr GetExpr() const { return expression; }
void SimplifyIte();
z3::expr CanonizeBoundVariables(const z3::expr&);
private:
z3::context* context;
......@@ -70,6 +71,7 @@ private:
BoundType getBoundType(z3::expr, const std::vector<BoundVar>&);
int getNumberOfLeadingZeroes(const z3::expr&);
int lastBound = 0;
};
#endif // UNCONSTRAINEDVARIABLESIMPLIFIER_H
#ifndef UNCONSTRAINEDVARIABLESIMPLIFIER_H
#define UNCONSTRAINEDVARIABLESIMPLIFIER_H
#include "z3++.h"
#include <map>
#include <vector>
#include <string>
#include <tuple>
enum BoundType { EXISTENTIAL, UNIVERSAL };
class UnconstrainedVariableSimplifier
{
public:
UnconstrainedVariableSimplifier(z3::context &ctx, z3::expr expr) : expression(expr)
{
this->context = &ctx;
variableCounts = countVariableOccurences(expression, std::vector<std::string>()).first;
}
void PrintUnconstrained()
{
bool allConstrained = true;
for (auto &item : variableCounts)
{
std::cout << "var " << item.first << " - " << item.second << " times" << std::endl;
if (item.second == 1)
{
allConstrained = false;
//std::cout << "Unconstrained variable: " << item.first << std::endl;
}
}
if (allConstrained) std::cout << "All variables constrained" << std::endl;
}
void SimplifyOnce()
{
expression = simplifyOnce(expression, {}, true);
}
z3::expr GetExpr() const { return expression; }
void SimplifyIte();
private:
z3::context* context;
z3::expr expression;
std::map<const Z3_ast, std::pair<std::map<std::string, int>, std::vector<std::string>>> subformulaVariableCounts;
std::map<const Z3_ast, int> subformulaMaxDeBruijnIndices;
std::map<std::string, int> variableCounts;
typedef std::pair<std::string, BoundType> boundVar;
typedef std::map<const Z3_ast, std::pair<z3::expr, const std::vector<boundVar>>> cacheMapType;
cacheMapType trueSimplificationCache;
cacheMapType falseSimplificationCache;
std::pair<std::map<std::string, int>, int> countVariableOccurences(z3::expr, std::vector<std::string>);
z3::expr simplifyOnce(z3::expr, std::vector<std::pair<std::string, BoundType>>, bool);
bool isUnconstrained(z3::expr, const std::vector<std::pair<std::string, BoundType>>&);
bool isVar(z3::expr);
bool isBefore(z3::expr, z3::expr);
BoundType getBoundType(z3::expr, const std::vector<std::pair<std::string, BoundType>>&);
int getNumberOfLeadingZeroes(const z3::expr&);
};
#endif // UNCONSTRAINEDVARIABLESIMPLIFIER_H
......@@ -20,17 +20,18 @@ int main(int argc, char* argv[])
{
static struct option long_options[] = {
{"propagate-unconstrained", no_argument, 0, 'p' },
{"canonize", no_argument, 0, 'c' },
{"run-z3", no_argument, 0, 'z' },
{0, 0, 0, 0 }
};
bool propagateUnconstrainedFlag = false, runZ3 = false;
bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false;
char* filename;
int opt = 0;
int long_index = 0;
while ((opt = getopt_long(argc, argv,"pz", long_options, &long_index )) != -1)
while ((opt = getopt_long(argc, argv,"pzc", long_options, &long_index )) != -1)
{
switch (opt)
{
......@@ -40,6 +41,9 @@ int main(int argc, char* argv[])
case 'z':
runZ3 = true;
break;
case 'c':
canonize = true;
break;
default:
std::cout << "Invalid arguments" << std::endl;
exit(1);
......@@ -62,10 +66,15 @@ int main(int argc, char* argv[])
e = e.simplify();
if (propagateUnconstrainedFlag)
if (canonize)
{
UnconstrainedVariableSimplifier simplifier(ctx, e);
e = simplifier.CanonizeBoundVariables(e);
}
if (propagateUnconstrainedFlag)
{
UnconstrainedVariableSimplifier simplifier(ctx, e);
//simplifier.PrintUnconstrained();
simplifier.SimplifyIte();
e = simplifier.GetExpr();
......@@ -78,6 +87,9 @@ int main(int argc, char* argv[])
{
solver s(ctx);
s.add(e);
params p(ctx);
p.set("smt.timeout", 5000u);
s.set(p);
std::cout << s.check() << std::endl;
}
else
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment