From d0e10929867d4f69443438a4cc20d91f49ea7ab3 Mon Sep 17 00:00:00 2001
From: Petr Rockai <me@mornfall.net>
Date: Thu, 30 Jan 2020 12:55:49 +0000
Subject: [PATCH] smt: Get rid of brq::smt_op::constraint.
---
divine/smt/builder-smtlib.cpp | 1 -
divine/smt/builder-stp.cpp | 1 -
divine/smt/builder-z3.cpp | 1 -
divine/smt/rpn.hpp | 5 +----
4 files changed, 1 insertion(+), 7 deletions(-)
diff --git a/divine/smt/builder-smtlib.cpp b/divine/smt/builder-smtlib.cpp
index b4b9b4d0b..5d6c4c543 100644
--- a/divine/smt/builder-smtlib.cpp
+++ b/divine/smt/builder-smtlib.cpp
@@ -241,7 +241,6 @@ SMTLib2::Node SMTLib2::binary( brq::smt_op op, Node a, Node b, int bw )
case op_t::bool_or:
case op_t::bv_or:
return define( _ctx.binop< op_t::bool_or >( 1, a, b ) );
- case op_t::constraint:
case op_t::bool_and:
case op_t::bv_and:
return define( _ctx.binop< op_t::bool_and >( 1, a, b ) );
diff --git a/divine/smt/builder-stp.cpp b/divine/smt/builder-stp.cpp
index e84c6e286..6679e244a 100644
--- a/divine/smt/builder-stp.cpp
+++ b/divine/smt/builder-stp.cpp
@@ -173,7 +173,6 @@ stp::ASTNode STP::binary( brq::smt_op op, Node a, Node b, int bw )
case op_t::bool_or:
case op_t::bv_or:
return _stp.CreateNode( stp::OR, a, b );
- case op_t::constraint:
case op_t::bool_and:
case op_t::bv_and:
return _stp.CreateNode( stp::AND, a, b );
diff --git a/divine/smt/builder-z3.cpp b/divine/smt/builder-z3.cpp
index c1a55e819..5d33cf5d4 100644
--- a/divine/smt/builder-z3.cpp
+++ b/divine/smt/builder-z3.cpp
@@ -211,7 +211,6 @@ z3::expr Z3::binary( brq::smt_op op, Node a, Node b, int )
case op_t::bv_or:
return a || b;
case op_t::bool_and:
- case op_t::constraint:
case op_t::bv_and:
return a && b;
case op_t::bv_uge:
diff --git a/divine/smt/rpn.hpp b/divine/smt/rpn.hpp
index 1285d7c42..a6b28f8ed 100644
--- a/divine/smt/rpn.hpp
+++ b/divine/smt/rpn.hpp
@@ -30,7 +30,7 @@
namespace divine::smt
{
template< typename builder_t, typename expr_t >
- auto evaluate( builder_t &bld, const expr_t &expr, bool *is_constraint = nullptr )
+ auto evaluate( builder_t &bld, const expr_t &expr )
{
using node_t = typename builder_t::Node;
@@ -54,9 +54,6 @@ namespace divine::smt
for ( auto &atom : expr )
{
- if ( is_constraint )
- *is_constraint = atom.op == brq::smt_op::constraint;
-
auto op = atom.op;
if ( atom.varid() ) push( bld.variable( atom.varid(), atom.bw() ), atom.bw() );
--
GitLab