smt: Get rid of brq::smt_op::constraint.

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 ) );

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 );

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:

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() );