replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Generalise operator-= and operator|= of guardt 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6352 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2016-02-16 17:34:12 +00:00
parent 67b6a7dd62
commit 35fc794357
1 changed files with 42 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

64
src/util/guard.cpp
View File

@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <ostream>
#include "std_expr.h"
#include "simplify_utils.h"
#include "guard.h"
/*******************************************************************\
@ -138,17 +139,23 @@ guardt &operator -= (guardt &g1, const guardt &g2)
if(g1.id()!=ID_and || g2.id()!=ID_and)
return g1;
sort_and_join(g1);
guardt g2_sorted=g2;
sort_and_join(g2_sorted);
exprt::operandst &op1=g1.operands();
const exprt::operandst &op2=g2.operands();
const exprt::operandst &op2=g2_sorted.operands();
exprt::operandst::const_iterator it2=op2.begin();
while(!op1.empty() &&
it2!=op2.end() &&
op1.front()==*it2)
exprt::operandst::iterator it1=op1.begin();
for(exprt::operandst::const_iterator
it2=op2.begin();
it2!=op2.end();
++it2)
{
op1.erase(op1.begin());
it2++;
while(it1!=op1.end() && *it1<*it2)
++it1;
if(it1!=op1.end() && *it1==*it2)
it1=op1.erase(it1);
}
g1=conjunction(op1);
@ -183,33 +190,43 @@ guardt &operator |= (guardt &g1, const guardt &g2)
else
g1=or_exprt(g1, g2);
// TODO: make simplify more capable and apply here
return g1;
}
// find common prefix
sort_and_join(g1);
guardt g2_sorted=g2;
sort_and_join(g2_sorted);
exprt::operandst &op1=g1.operands();
const exprt::operandst &op2=g2.operands();
const exprt::operandst &op2=g2_sorted.operands();
exprt::operandst n_op1, n_op2;
n_op1.reserve(op1.size());
n_op2.reserve(op2.size());
exprt::operandst::iterator it1=op1.begin();
exprt::operandst::const_iterator it2=op2.begin();
while(it1!=op1.end())
for(exprt::operandst::const_iterator
it2=op2.begin();
it2!=op2.end();
++it2)
{
if(it2==op2.end())
break;
if(*it1!=*it2)
break;
it1++;
it2++;
while(it1!=op1.end() && *it1<*it2)
{
n_op1.push_back(*it1);
it1=op1.erase(it1);
}
if(it1!=op1.end() && *it1==*it2)
++it1;
else
n_op2.push_back(*it2);
}
if(it2==op2.end()) return g1;
if(n_op2.empty()) return g1;
// end of common prefix
exprt::operandst n_op1(it1, op1.end());
exprt::operandst n_op2(it2, op2.end());
exprt and_expr1=conjunction(n_op1);
exprt and_expr2=conjunction(n_op2);
@ -225,6 +242,7 @@ guardt &operator |= (guardt &g1, const guardt &g2)
{
}
else
// TODO: make simplify more capable and apply here
g1.add(or_exprt(and_expr1, and_expr2));
}