Question about make_term()

[ZhiyuanYan]

Hello. I am trying to use the make_term(). However, I find that there is some different when using this function. For example, when I use the ts_.make_term(And, prop, eq). Sometime program will synthesis the "bvand", and program will generate something like "ite" format to represent the equal value. However, when I trying to create a new solver, I found that I cannot get the same format, the program can only synthesis "and" and cannot synthesis "ite". I want to know why this will happen? Do I need to set other options to get the former format? The solver I am using is the Boolector.

Thank you very much!

[yoni206]

Hi and thanks for your question!
We will be happy to help, but it isn't entirely clear what the problem is.
Would it be possible for you to post here a minimal program that uses smt-switch, so that we can try and reproduce the issue?

[ZhiyuanYan]

Hi, thank you for your reply!
The first program is:

`    for (const auto & var_val_pair : GetCex() ) {
    const auto & var_name = var_val_pair.first;
    auto pos = ts_.named_terms().find(var_name);
    assert(pos != ts_.named_terms().end());
    auto var = pos->second;
    auto sort = var->get_sort();
    auto val = ts_.make_term(var_val_pair.second, sort, 2);
    auto eq = ts_.make_term(Equal, var, val);
    if (prop == nullptr)
      prop = eq;
    else
      prop = ts_.make_term(And, prop, eq);
  }`

And it will generate a result:

And the second program is:

`      if (t->is_symbol()){
        var_wrapper = "RTL." + t->to_string();
        // auto sort = t->get_sort()->get_sort_kind();
        auto sort_new = solver->make_sort(sort,bit_width);
        term_wrapper = solver->make_symbol(var_wrapper,sort_new);
        count_var = count_var + 1;
      }
      else if (t->is_value()){
        auto sort_new = solver->make_sort(sort,bit_width);
        auto val_string = t->to_string(); 
        val_string = val_string.substr(2, val_string.size()-1);
        val = solver->make_term(val_string,sort_new,2);
        count_val = count_val + 1;
      }
      if ((count_val == 1 )&&(count_var == 1)){
                eq = solver->make_term(Equal, term_wrapper, val );
                if(new_Term == nullptr)
                {
                new_Term = eq;
                }
                else{
                  new_Term = solver->make_term(And, new_Term,eq);
                }
                count_val = 0;
                count_var = 0;
      }`

And it will generate the result:

Actually, what I need to do is to extract the symbol in the first figure and change the name of the symbol, and finally push it back. As a consequence, I try to create a new solver to achieve it. However, the new term's format is different compared to original one.

Thank you very much and I am looking forward to your reply!

[yoni206]

Thanks for posting more details.

The examples are still a bit complicated and not self-contained enough to reproduce.

But, it sounds like the following solution could help:
Create a logging solver, rather than a regular solver.
This is done as follows:
https://github.com/stanford-centaur/smt-switch/blob/master/examples/btor_qf_ufbv.cpp#L12

Instead of passing false, pass true.

If that doesn't work, please try to provide a minimal runnable working example.

[ZhiyuanYan]

Hi, I think it can work now.

Thank you for your patience and guidance!

[ZhiyuanYan]

Hello, I have another issue. That is when I get a new term, then the function will be finished. At this time, the destructor function of the solver will be launched. However, there is another mistake, which is "'sort' is not a valid sort". Like the previous program, I tried to change the symbol name by traversing all the symbols and create a new solver to make new term.
However, it seems that destructor function fails to destruct this new solver. Can you please tell me what is the meaning of this bug and the potential way to solve this bug?

If you need other information, please let me know and I will try my best to provide to you.

Thank you very much and I am looking forward to your reply!

[yoni206]

Hi, thanks for raising this new issue.
It is not clear to me where the problem is, though.
Please try to create a minimal working example in a single cpp file which I could then try to reproduce.

[ZhiyuanYan]

Thank you for your reply!

I felt sorry that I tried my best to create a single cpp file. However, the original file is large. And I cannot create a minial example now. I try best to create a cpp file. The "invar" is a term that I got in the previous solver. And now I want to change the symbol name in the "invar", so I try to create a new solver, and use the function called name_changed() to traverse all the symbols in the "invar", and make a new term. Finally, I use the function called smt_lib2_front() to tranfer the new term into SMTLIB2 format. The attachment is the term "invar".

I hope it can work for you. If it it not clear for you, I will continue to try my best to describe this problem.

Thank you very much!

#include <iostream>
#include "assert.h"

#ifdef WITH_PROFILING
#include <gperftools/profiler.h>
#endif

#include "smt-switch/boolector_factory.h"
#include "smt-switch/logging_solver.h"
#include "smt-switch/smtlib_reader.h"
#include "smt/available_solvers.h"
#include "utils/logger.h"
#include "utils/ts_analysis.h"
#include "utils/term_analysis.h"
using namespace pono;
using namespace smt;
using namespace std;

void name_changed(const Term & term, Term & new_Term, smt::SmtSolver &solver)
{
  TermVec to_visit({ term });
  // SortKind sort;
  Term t;
  Term val;
  Term eq;
  Term term_wrapper;
  Term var_record;
  int count_var=0;
  int count_val=0;
  int not_count = 0;
  std::string var_wrapper;
  int var_width;
  int val_width;
  while (!to_visit.empty()) {
    t = to_visit.back();
    to_visit.pop_back();

    for (const auto & tt : t) {
      to_visit.push_back(tt);
    }

    if (t->get_op() == BVNot){
      not_count = 1;
    }
    if (t->get_op().is_null()) {
      assert(t->is_symbol() || t->is_value());
      auto sort = t->get_sort()->get_sort_kind();
      auto bit_width = t->get_sort()->get_width();

      if (t->is_symbol()){
        var_wrapper = "RTL." + t->to_string();
// auto sort = t->get_sort()->get_sort_kind();
        auto sort_new = solver->make_sort(sort,bit_width);
        term_wrapper = solver->make_symbol(var_wrapper,sort_new);
        if (bit_width == 1){
          var_record = term_wrapper;
        }  
        count_var = count_var + 1;
        var_width = bit_width;
      }
      else if (t->is_value()){
        auto sort_new = solver->make_sort(sort,bit_width);
        auto val_string = t->to_string(); 
        val_string = val_string.substr(2, val_string.size()-1);
        val = solver->make_term(val_string,sort_new,2);
        count_val = count_val + 1;
        val_width = bit_width;
      }
      
      if ((count_val == 1 )&&(count_var == 1)&&(var_width == val_width)){
                eq = solver->make_term(Equal, term_wrapper, val );
                if(new_Term == nullptr)
                {
                new_Term = eq;
                }
                else{
                  new_Term = solver->make_term(BVAnd, new_Term,eq);
                }
                count_val = 0;
                count_var = 0;
                not_count = 0;
      }
      /// The val may occur two times, which means that originally, they are 1 bit vector./////
      else{
                if((var_width != 1)) continue; 
                if (not_count ==1){
                  not_count = 0;
                  eq = solver->make_term(BVNot, var_record);
                }
                else{
                  eq = var_record;
                }
                if(new_Term == nullptr)
                {
                  new_Term = eq;
                }
                else{
                  new_Term = solver->make_term(BVAnd, new_Term,eq);
                }
                count_var = count_var -1;
                assert(count_var = 1);
      }
    }
  }
  new_Term = solver -> make_term(BVNot, new_Term);
  cout<<new_Term<<endl;
}

void smt_lib2_front(const UnorderedTermSet out,std::string & sort_list){
      UnorderedTermSortMap symbols_mapping;
      for (const auto &var: out){
          std::cout<<var<<std::endl;
          auto var_sort = var->get_sort();
          symbols_mapping.insert(pair<Term,Sort> (var,var_sort));
      }
      for (const auto &symbols: symbols_mapping){
        sort_list = sort_list + "(" + "|" + symbols.first->to_string() + "|" + " " + symbols.second->to_string() + ")" +" ";
        cout<<sort_list<<endl;
      }
}

int main(){
    smt::UnorderedTermSet out;
    Term new_Term;
    std::string var_wrapper;
    std::string sort_list = "";
    smt::SmtSolver solver  = BoolectorSolverFactory::create(true);
    solver->set_logic("BV");
    solver->set_opt("incremental", "false");
    solver->set_opt("produce-models", "false");
    name_changed(invar, new_Term,solver);
    out = get_free_symbols(new_Term);
    smt_lib2_front(out,sort_list);

    

    return 0; //return
  }

[yoni206]

Hi, I've tried to look at this example, but it is hard to pinpoint where the problem is. If you send a small example, that would improve things and then we might be able to find the problem.

[Ashu1815]

For anyone landing here from a search: the fix in this thread was to enable
logging on the solver, and I've tried to make that discoverable rather than
leaving it in a comment inside one example.

Opened #509, which adds docs/sorts-and-operators.md recording the answer and
why it works. Briefly:

Two separate things make a term built with And come back looking different on
Boolector, and examples/btor_qf_ufbv.cpp:8 names both:

1. Sort aliasing. Boolector has no boolean sort. make_sort(BOOL) returns a
   width-1 bit-vector sort (btor/src/boolector_solver.cpp:497), and
   get_value handles BV and BOOL together (:352). So a BOOL term
   genuinely is a bit-vector term, and printing reflects that.
2. On-the-fly rewriting. Boolector simplifies as terms are built, so the
   structure returned need not match the structure requested.

BoolectorSolverFactory::create(true) addresses both, because LoggingSolver
keeps smt-switch's own term DAG alongside the backend's.

The doc also covers what stays portable across backends (SortKind and the
answers of check_sortedness) versus what does not (the backend's printed
form), since that distinction is the thing that makes the behaviour surprising
in the first place.

Corrections welcome on the PR if I've mischaracterised anything.