<commit_before>// -*- c++ -*-
/********************************************************************
 * AUTHORS: <NAME>, <NAME>
 *
 * BEGIN DATE: November, 2005
 *
 * LICENSE: Please view LICENSE file in the home dir of this Program
 ********************************************************************/

#include <assert.h>
#include <math.h>
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
#include "AbsRefine_CounterExample.h"

namespace BEEV
{
  using std::pair;
  using std::map;

  /******************************************************************
   * Abstraction Refinement related functions
   ******************************************************************/  

    enum Polarity
    {
        LEFT_ONLY, RIGHT_ONLY, BOTH
    };

    void
    getSatVariables(const ASTNode & a, vector<unsigned> & v_a, SATSolver & SatSolver,
            ToSATBase::ASTNodeToSATVar & satVar)
    {
        ToSATBase::ASTNodeToSATVar::iterator it = satVar.find(a);
        if (it != satVar.end())
            v_a = it->second;
        else if (!a.isConstant())
            {
                assert(a.GetKind() == SYMBOL);
                // It was ommitted from the initial problem, so assign it freshly.
                for (unsigned i = 0; i < a.GetValueWidth(); i++)
                    {
                        uint32_t v = SatSolver.newVar();
                        // We probably don't want the variable eliminated.
                        SatSolver.setFrozen(v);
                        v_a.push_back(v);
                    }
                satVar.insert(make_pair(a, v_a));
            }
    }


    // This function adds the clauses to constrain that "a" and "b" equal a fresh variable
    // (which it returns).
    // Because it's used to create array axionms (a=b)-> (c=d), it can be
    // used to only add one of the two polarities.
    Minisat::Var
    getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar,
            Polarity polary = BOTH)
    {
        const unsigned width = a.GetValueWidth();
        assert(width == b.GetValueWidth());
        assert(!a.isConstant() || !b.isConstant());

        vector<unsigned> v_a;
        vector<unsigned> v_b;

        getSatVariables(a, v_a, SatSolver, satVar);
        getSatVariables(b, v_b, SatSolver, satVar);

        // The only time v_a or v_b will be empty is if "a" resp. "b" is a constant.

        if (v_a.size() == width && v_b.size() == width)
            {
                SATSolver::vec_literals all;
                const int result = SatSolver.newVar();

                for (unsigned i = 0; i < width; i++)
                    {
                        SATSolver::vec_literals s;

                        if (polary != RIGHT_ONLY)
                            {
                                int nv0 = SatSolver.newVar();
                                s.push(SATSolver::mkLit(v_a[i], true));
                                s.push(SATSolver::mkLit(v_b[i], true));
                                s.push(SATSolver::mkLit(nv0, false));
                                SatSolver.addClause(s);
                                s.clear();

                                s.push(SATSolver::mkLit(v_a[i], false));
                                s.push(SATSolver::mkLit(v_b[i], false));
                                s.push(SATSolver::mkLit(nv0, false));
                                SatSolver.addClause(s);
                                s.clear();

                                all.push(SATSolver::mkLit(nv0, true));
                            }

                        if (polary != LEFT_ONLY)
                            {
                                s.push(SATSolver::mkLit(v_a[i], true));
                                s.push(SATSolver::mkLit(v_b[i], false));
                                s.push(SATSolver::mkLit(result, true));
                                SatSolver.addClause(s);
                                s.clear();

                                s.push(SATSolver::mkLit(v_a[i], false));
                                s.push(SATSolver::mkLit(v_b[i], true));
                                s.push(SATSolver::mkLit(result, true));
                                SatSolver.addClause(s);
                                s.clear();
                            }
                    }
                if (all.size() > 0)
                {
                        all.push(SATSolver::mkLit(result, false));
                        SatSolver.addClause(all);
                }
                return result;
            }
        else if ((v_a.size() == 0) ^ (v_b.size()) == 0)
            {
                ASTNode constant = a.isConstant() ? a : b;
                vector<unsigned> vec = v_a.size() == 0 ? v_b : v_a;
                assert(constant.isConstant());
                assert(vec.size() == width);

                SATSolver::vec_literals all;
                const int result = SatSolver.newVar();
                all.push(SATSolver::mkLit(result, false));

                CBV v = constant.GetBVConst();
                for (unsigned i = 0; i < width; i++)
                    {
                        if (polary != RIGHT_ONLY)
                            {
                                if (CONSTANTBV::BitVector_bit_test(v, i))
                                    all.push(SATSolver::mkLit(vec[i], true));
                                else
                                    all.push(SATSolver::mkLit(vec[i], false));
                            }

                        if (polary != LEFT_ONLY)
                            {
                                SATSolver::vec_literals p;
                                p.push(SATSolver::mkLit(result, true));
                                if (CONSTANTBV::BitVector_bit_test(v, i))
                                    p.push(SATSolver::mkLit(vec[i], false));
                                else
                                    p.push(SATSolver::mkLit(vec[i], true));

                                SatSolver.addClause(p);<commit_msg>Fixing a bug I just introduced while fixing warnings<commit_after>// -*- c++ -*-
/********************************************************************
 * AUTHORS: <NAME>, <NAME>
 *
 * BEGIN DATE: November, 2005
 *
 * LICENSE: Please view LICENSE file in the home dir of this Program
 ********************************************************************/

#include <assert.h>
#include <math.h>
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
#include "AbsRefine_CounterExample.h"

namespace BEEV
{
  using std::pair;
  using std::map;

  /******************************************************************
   * Abstraction Refinement related functions
   ******************************************************************/  

    enum Polarity
    {
        LEFT_ONLY, RIGHT_ONLY, BOTH
    };

    void
    getSatVariables(const ASTNode & a, vector<unsigned> & v_a, SATSolver & SatSolver,
            ToSATBase::ASTNodeToSATVar & satVar)
    {
        ToSATBase::ASTNodeToSATVar::iterator it = satVar.find(a);
        if (it != satVar.end())
            v_a = it->second;
        else if (!a.isConstant())
            {
                assert(a.GetKind() == SYMBOL);
                // It was ommitted from the initial problem, so assign it freshly.
                for (unsigned i = 0; i < a.GetValueWidth(); i++)
                    {
                        uint32_t v = SatSolver.newVar();
                        // We probably don't want the variable eliminated.
                        SatSolver.setFrozen(v);
                        v_a.push_back(v);
                    }
                satVar.insert(make_pair(a, v_a));
            }
    }


    // This function adds the clauses to constrain that "a" and "b" equal a fresh variable
    // (which it returns).
    // Because it's used to create array axionms (a=b)-> (c=d), it can be
    // used to only add one of the two polarities.
    Minisat::Var
    getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar,
            Polarity polary = BOTH)
    {
        const unsigned width = a.GetValueWidth();
        assert(width == b.GetValueWidth());
        assert(!a.isConstant() || !b.isConstant());

        vector<unsigned> v_a;
        vector<unsigned> v_b;

        getSatVariables(a, v_a, SatSolver, satVar);
        getSatVariables(b, v_b, SatSolver, satVar);

        // The only time v_a or v_b will be empty is if "a" resp. "b" is a constant.

        if (v_a.size() == width && v_b.size() == width)
            {
                SATSolver::vec_literals all;
                const int result = SatSolver.newVar();

                for (unsigned i = 0; i < width; i++)
                    {
                        SATSolver::vec_literals s;

                        if (polary != RIGHT_ONLY)
                            {
                                int nv0 = SatSolver.newVar();
                                s.push(SATSolver::mkLit(v_a[i], true));
                                s.push(SATSolver::mkLit(v_b[i], true));
                                s.push(SATSolver::mkLit(nv0, false));
                                SatSolver.addClause(s);
                                s.clear();

                                s.push(SATSolver::mkLit(v_a[i], false));
                                s.push(SATSolver::mkLit(v_b[i], false));
                                s.push(SATSolver::mkLit(nv0, false));
                                SatSolver.addClause(s);
                                s.clear();

                                all.push(SATSolver::mkLit(nv0, true));
                            }

                        if (polary != LEFT_ONLY)
                            {
                                s.push(SATSolver::mkLit(v_a[i], true));
                                s.push(SATSolver::mkLit(v_b[i], false));
                                s.push(SATSolver::mkLit(result, true));
                                SatSolver.addClause(s);
                                s.clear();

                                s.push(SATSolver::mkLit(v_a[i], false));
                                s.push(SATSolver::mkLit(v_b[i], true));
                                s.push(SATSolver::mkLit(result, true));
                                SatSolver.addClause(s);
                                s.clear();
                            }
                    }
                if (all.size() > 0)
                {
                        all.push(SATSolver::mkLit(result, false));
                        SatSolver.addClause(all);
                }
                return result;
            }
        else if ((v_a.size() == 0) ^ (v_b.size() == 0))
            {
                ASTNode constant = a.isConstant() ? a : b;
                vector<unsigned> vec = v_a.size() == 0 ? v_b : v_a;
                assert(constant.isConstant());
                assert(vec.size() == width);

                SATSolver::vec_literals all;
                const int result = SatSolver.newVar();
                all.push(SATSolver::mkLit(result, false));

                CBV v = constant.GetBVConst();
                for (unsigned i = 0; i < width; i++)
                    {
                        if (polary != RIGHT_ONLY)
                            {
                                if (CONSTANTBV::BitVector_bit_test(v, i))
                                    all.push(SATSolver::mkLit(vec[i], true));
                                else
                                    all.push(SATSolver::mkLit(vec[i], false));
                            }

                        if (polary != LEFT_ONLY)
                            {
                                SATSolver::vec_literals p;
                                p.push(SATSolver::mkLit(result, true));
                                if (CONSTANTBV::BitVector_bit_test(v, i))
                                    p.push(SATSolver::mkLit(vec[i], false));
                                else
                                    p.push(SATSolver::mkLit(vec[i], true));

                                SatSolver.addClause(p);
{'fraction_non_alphanumeric': 0.1527880127732744, 'fraction_numerical': 0.002783918775075739, 'mean_word_length': 1.2011173184357542, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 25, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 14, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3628381', 'n_tokens_mistral': 3530, 'n_tokens_neox': 3181, 'n_words': 661}