cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Make Real sort available in SMTChecker

Browse Source
This commit is contained in:
hrkrshnn 2020-12-29 19:31:59 +01:00
parent f7624dff66
commit 0d6adef834
4 changed files with 20 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/SMTLib2Interface.cpp
View File

@ -244,6 +244,8 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
return tupleName;
}
case Kind::Real:
return "Real";
default:
smtAssert(false, "Invalid SMT sort");
}

2
libsmtutil/Sorts.cpp
View File

@ -18,6 +18,7 @@
#include <libsmtutil/Sorts.h>
#include <memory>
using namespace std;
@ -36,5 +37,6 @@ shared_ptr<IntSort> SortProvider::intSort(bool _signed)
}
shared_ptr<BitVectorSort> const SortProvider::bitVectorSort{make_shared<BitVectorSort>(256)};
shared_ptr<RealSort> const SortProvider::realSort{make_shared<RealSort>()};
}

15
libsmtutil/Sorts.h
View File

@ -36,7 +36,8 @@ enum class Kind
Function,
Array,
Sort,
Tuple
Tuple,
Real
};
struct Sort
@ -65,6 +66,17 @@ struct IntSort: public Sort
bool isSigned;
};
struct RealSort: public Sort
{
RealSort(): Sort(Kind::Real)
{}
bool operator==(RealSort const& _other) const
{
return Sort::operator==(_other);
}
};
struct BitVectorSort: public Sort
{
BitVectorSort(unsigned _size):
@ -196,6 +208,7 @@ struct SortProvider
static std::shared_ptr<IntSort> const sintSort;
static std::shared_ptr<IntSort> intSort(bool _signed = false);
static std::shared_ptr<BitVectorSort> const bitVectorSort;
static std::shared_ptr<RealSort> const realSort;
};
}

2
libsmtutil/Z3Interface.cpp
View File

@ -385,6 +385,8 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
);
return tupleConstructor.range();
}
case Kind::Real:
return m_context.real_sort();
default:
break;