Commit 1c9c51c4 authored by Henrich Lauko's avatar Henrich Lauko

smt: Rework smt extract to work with RPN representation.

parent 87cc4a9e
......@@ -24,33 +24,7 @@ namespace divine::smt
template< typename Builder >
typename Builder::Node Extract< Builder >::build( vm::HeapPointer p )
{
auto f = read( p );
if ( isUnary( f->op() ) )
{
auto arg = convert( f->unary.child );
return this->unary( f->unary, arg );
}
if ( isBinary( f->op() ) )
{
auto a = convert( f->binary.left ), b = convert( f->binary.right );
return this->binary( f->binary, a, b );
}
switch ( f->op() )
{
case sym::Op::Variable:
return this->variable( f->var.type, f->var.id );
case sym::Op::Constant:
switch ( f->con.type.type() ) {
case sym::Type::Int:
return this->constant( f->con.type, f->con.value );
case sym::Type::Float:
return this->constant( f->con.type, static_cast< double >( f->con.value ) );
}
default: UNREACHABLE_F( "unexpected operation %d", f->op() );
}
return evaluate( *this, read( p ) );
}
template struct Extract< builder::SMTLib2 >;
......
......@@ -20,7 +20,7 @@
#include <divine/vm/memory.hpp>
#include <divine/smt/builder.hpp>
#include <lart/lart.h>
#include <divine/smt/rpn.hpp>
namespace divine::smt
{
......@@ -35,9 +35,11 @@ struct Extract : Builder
: Builder( std::forward< Args >( args )... ), _heap( heap )
{}
lart::sym::Formula *read( vm::HeapPointer ptr )
RPN read( vm::HeapPointer ptr )
{
return reinterpret_cast< lart::sym::Formula * >( _heap.unsafe_bytes( ptr ).begin() );
auto term = *reinterpret_cast< vm::HeapPointer * >( _heap.unsafe_bytes( ptr ).begin() );
auto data = _heap.unsafe_bytes( ptr );
return RPN{ { data.begin(), data.end() } };
}
Node build( vm::HeapPointer p );
......
Markdown is supported
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