Commit 27d93ad1 authored by Henrich Lauko's avatar Henrich Lauko

smt: Let smt builders work with RPN formula representation.

parent 1c9c51c4
......@@ -2,7 +2,7 @@
/*
* (c) 2018 Petr Ročkai <code@fixp.eu>
* (c) 2018 Henrich Lauko <xlauko@mail.muni.cz>
* (c) 2018-2019 Henrich Lauko <xlauko@mail.muni.cz>
*
* Permission to use, copy, modify, and distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
......@@ -19,25 +19,32 @@
#pragma once
#include <lart/lart.h>
#include <variant>
#include <divine/smt/rpn.hpp>
#include <divine/vm/divm.h>
#include <brick-smt>
namespace divine::smt { namespace sym = lart::sym; }
namespace divine::smt::builder
{
using RPN = divine::smt::RPN;
using Operation = RPN::Operation;
using Op = brick::smt::Op;
template< typename B >
auto mk_bin( B &bld, sym::Op op, int bw, typename B::Node a, typename B::Node b )
{
return bld.binary( sym::Binary( op, sym::Type( sym::Type::Int, bw ), vm::nullPointer(),
vm::nullPointer() ),
a, b );
}
template< typename Builder >
auto mk_bin( Builder &bld, Op op, int bw, typename Builder::Node a, typename Builder::Node b )
-> typename Builder::Node
{
ASSERT( RPN::is_binary( op ) );
return bld.binary( Operation{ op, bw }, a, b );
}
template< typename B >
auto mk_un( B &bld, sym::Op op, int bw, typename B::Node a )
{
return bld.unary( sym::Unary( op, sym::Type( sym::Type::Int, bw ), vm::nullPointer() ), a );
}
template< typename Builder >
auto mk_un( Builder &bld, Op op, int bw, typename Builder::Node a )
-> typename Builder::Node
{
ASSERT( RPN::is_unary( op ) );
return bld.unary( Operation{ op, bw }, a );
}
} // namespace divine::smt::builder
This diff is collapsed.
......@@ -30,11 +30,11 @@ struct SMTLib2
SMTLib2( brick::smt::Context &ctx, std::string suff = "", bool defs = true )
: _ctx( ctx ), _suff( suff ), _use_defs( defs ) {}
Node unary( sym::Unary un, Node n );
Node binary( sym::Binary bin, Node a, Node b );
Node constant( sym::Type t, uint64_t val );
Node unary( Operation op, Node n );
Node binary( Operation op, Node a, Node b );
Node constant( Constant con );
Node constant( bool );
Node variable( sym::Type t, int32_t id );
Node variable( Variable var );
Node define( Node def );
brick::smt::Context &_ctx;
......
......@@ -20,6 +20,7 @@
#include <divine/smt/builder-stp.hpp>
#if 0
#if OPT_STP
namespace divine::smt::builder
{
......@@ -191,3 +192,4 @@ stp::ASTNode STP::binary( sym::Binary bin, Node a, Node b )
}
#endif
#endif
......@@ -26,6 +26,7 @@
namespace divine::smt::builder
{
#if 0
struct STP
{
using Node = stp::ASTNode;
......@@ -41,6 +42,22 @@ struct STP
STP( stp::STPMgr &stp ) : _stp( stp ) {}
stp::STPMgr &_stp;
};
#endif
struct STP
{
using Node = stp::ASTNode;
STP( stp::STPMgr &stp ) : _stp( stp ) {}
Node unary( Operation, Node ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
Node binary( Operation, Node, Node ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
Node constant( Constant ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
Node constant( bool ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
Node variable( Variable ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
stp::STPMgr &_stp;
};
} // namespace divine::smt::builder
#endif
......@@ -19,7 +19,7 @@
*/
#include <divine/smt/builder-z3.hpp>
#if 0
#if OPT_Z3
namespace divine::smt::builder
{
......@@ -249,3 +249,4 @@ z3::expr Z3::binary( sym::Binary bin, Node a, Node b )
} // namespace divine::smtl::builder
#endif
#endif
......@@ -26,6 +26,7 @@
namespace divine::smt::builder
{
#if 0
struct Z3
{
using Node = z3::expr;
......@@ -39,6 +40,21 @@ struct Z3
z3::context &_ctx;
};
#endif
struct Z3
{
using Node = z3::expr;
Z3( z3::context &c ) : _ctx( c ) {}
Node unary( Operation, Node ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
Node binary( Operation, Node, Node ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
Node constant( Constant ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
Node constant( bool ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
Node variable( Variable ) { UNREACHABLE_F( "NOT IMPLEMENTED" ); }
z3::context &_ctx;
};
} // namespace divine::smt::builder
#endif
......@@ -24,4 +24,3 @@
#include <divine/smt/builder-stp.hpp>
#include <divine/smt/builder-z3.hpp>
......@@ -5,16 +5,18 @@
#include <brick-proc>
#include <brick-bitlevel>
using namespace divine::smt::builder;
namespace divine::smt::solver
{
namespace smt = brick::smt;
namespace proc = brick::proc;
bool match( sym::Constant &a, sym::Constant &b )
bool match( const Constant &a, const Constant &b )
{
const auto mask = brick::bitlevel::ones< uint64_t >( a.type.bitwidth() );
return a.type.bitwidth() == b.type.bitwidth() && ( a.value & mask ) == ( b.value & mask );
const auto mask = brick::bitlevel::ones< uint64_t >( a.bitwidth );
return a.bitwidth == b.bitwidth && ( a.value & mask ) == ( b.value & mask );
}
Result SMTLib::solve()
......@@ -23,7 +25,7 @@ Result SMTLib::solve()
auto q = b.constant( true );
for ( auto clause : _asserts )
q = builder::mk_bin( b, sym::Op::And, 1, q, clause );
q = builder::mk_bin( b, Op::And, 1, q, clause );
auto r = brick::proc::spawnAndWait( proc::StdinString( _ctx.query( q ) ) | proc::CaptureStdout |
proc::CaptureStderr, _opts );
......@@ -45,17 +47,17 @@ Result SMTLib::solve()
template< typename Extract >
auto get_pc( Extract &e, vm::HeapPointer ptr )
{
auto query = e.constant( true );
return evaluate( e, e.read( ptr ) );
}
while ( !ptr.null() )
{
auto f = e.read( ptr );
auto clause = e.convert( f->binary.left );
query = builder::mk_bin( e, sym::Op::And, 1, query, clause );
ptr = f->binary.right;
}
return query;
template< typename Core, typename Node >
Op equality( const Node& node ) noexcept
{
if constexpr ( std::is_same_v< Core, STP > )
return Op::Eq;
else
return node.is_bv() || node.is_bool() ? Op::Eq : Op::FpOEQ;
}
template< typename Core >
......@@ -69,42 +71,38 @@ bool Simple< Core >::equal( SymPairs &sym_pairs, vm::CowHeap &h_1, vm::CowHeap &
auto c_1 = e_1.constant( true ), c_2 = e_2.constant( true );
bool constraints_found = false;
using namespace builder;
for ( auto p : sym_pairs )
for ( auto [lhs, rhs] : sym_pairs )
{
auto f_1 = e_1.read( p.first ), f_2 = e_2.read( p.second );
if ( f_1->op() == sym::Op::Constraint )
auto f_1 = e_1.read( lhs );
auto f_2 = e_2.read( rhs );
if ( f_1.is_constraint() )
{
ASSERT( !constraints_found );
ASSERT_EQ( int( f_2->op() ), int( sym::Op::Constraint ) );
ASSERT( f_2.is_constraint() );
constraints_found = true;
c_1 = get_pc( e_1, p.first );
c_2 = get_pc( e_2, p.second );
c_1 = get_pc( e_1, lhs );
c_2 = get_pc( e_2, rhs );
}
else
{
auto v_1 = e_1.convert( p.first ), v_2 = e_2.convert( p.second );
auto v_1 = e_1.convert( lhs );
auto v_2 = e_2.convert( rhs );
sym::Op op;
if constexpr ( std::is_same_v< Core, STP > )
op = sym::Op::EQ;
else
op = v_1.is_bv() || v_1.is_bool() ? sym::Op::EQ : sym::Op::FpOEQ;
Op op = equality< Core >( v_1 );
auto pair_eq = mk_bin( b, op, 1, v_1, v_2 );
v_eq = mk_bin( b, sym::Op::And, 1, v_eq, pair_eq );
v_eq = mk_bin( b, Op::And, 1, v_eq, pair_eq );
}
}
/* we already know that both constraint sets are sat */
auto c_eq = mk_bin( b, sym::Op::EQ, 1, c_1, c_2 ),
pc_fail = mk_un( b, sym::Op::BoolNot, 1, c_1 ),
v_eq_c = mk_bin( b, sym::Op::Or, 1, pc_fail, v_eq ),
eq = mk_bin( b, sym::Op::And, 1, c_eq, v_eq_c );
auto c_eq = mk_bin( b, Op::Eq, 1, c_1, c_2 ),
pc_fail = mk_un( b, Op::Not, 1, c_1 ),
v_eq_c = mk_bin( b, Op::Or, 1, pc_fail, v_eq ),
eq = mk_bin( b, Op::And, 1, c_eq, v_eq_c );
this->add( mk_un( b, sym::Op::BoolNot, 1, eq ) );
this->add( mk_un( b, Op::Not, 1, eq ) );
auto r = this->solve();
this->reset();
return r == Result::False;
......@@ -131,8 +129,9 @@ bool Caching< Core >::feasible( vm::CowHeap &heap, vm::HeapPointer ptr )
}
template< typename Core >
bool Incremental< Core >::feasible( vm::CowHeap &heap, vm::HeapPointer ptr )
bool Incremental< Core >::feasible( vm::CowHeap &/*heap*/, vm::HeapPointer /*ptr*/ )
{
#if 0
auto e = this->extract( heap );
auto query = e.constant( true );
std::unordered_set< vm::HeapPointer > in_context{ _inc.begin(), _inc.end() };
......@@ -142,7 +141,7 @@ bool Incremental< Core >::feasible( vm::CowHeap &heap, vm::HeapPointer ptr )
{
auto f = e.read( ptr );
auto clause = e.convert( f->binary.left );
query = mk_bin( e, sym::Op::And, 1, query, clause );
query = mk_bin( e, Op::And, 1, query, clause );
ptr = f->binary.right;
}
......@@ -169,6 +168,7 @@ bool Incremental< Core >::feasible( vm::CowHeap &heap, vm::HeapPointer ptr )
this->pop();
return result != Result::False;
#endif
}
#if OPT_STP
......
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