#include "expr/datatype.h"
#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
+#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_attributes.h"
int carg = -1;
int karg = -1;
// first, do standard minimizations
- Node min_t = d_qe->getTermDatabaseSygus()->minimizeBuiltinTerm( t );
+ Node min_t = minimizeBuiltinTerm(t);
Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl;
//check if op is in syntax sort
carg = d_qe->getTermDatabaseSygus()->getOpConsNum( stn, min_t );
return true;
}
- /*
- //flatten ITEs if necessary TODO : carry assignment or move this elsewhere
- if( t.getKind()==ITE ){
- TypeNode cstn = tds->getArgType( dt[karg], 0 );
- tds->registerSygusType( cstn );
- Node prev_t;
- while( !tds->hasKind( cstn, t[0].getKind() ) && t!=prev_t ){
- prev_t = t;
- Node exp_c = tds->expandBuiltinTerm( t[0] );
- if( !exp_c.isNull() ){
- t = NodeManager::currentNM()->mkNode( ITE, exp_c, t[1], t[2] );
- Trace("csi-rcons-debug") << "Pre expand to " << t << std::endl;
- }
- t = flattenITEs( t, false );
- if( t!=prev_t ){
- Trace("csi-rcons-debug") << "Flatten ITE to " << t << std::endl;
- std::map< Node, bool > sassign;
- std::vector< Node > svars;
- std::vector< Node > ssubs;
- t = simplifySolutionNode( t, sassign, svars, ssubs, 0 );
- }
- Assert( t.getKind()==ITE );
- }
- }
- */
-
Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id,
bool mod_eq)
{
if (rcons_depth < 1000)
{
// accelerated, recursive reconstruction of constants
- Kind pk = tds->getPlusKind(TypeNode::fromType(dt.getSygusType()));
+ Kind pk = getPlusKind(TypeNode::fromType(dt.getSygusType()));
if (pk != UNDEFINED_KIND)
{
int arg = tds->getKindConsNum(tn, pk);
if (arg != -1)
{
Kind ck =
- tds->getComparisonKind(TypeNode::fromType(dt.getSygusType()));
+ getComparisonKind(TypeNode::fromType(dt.getSygusType()));
Kind pkm =
- tds->getPlusKind(TypeNode::fromType(dt.getSygusType()), true);
+ getPlusKind(TypeNode::fromType(dt.getSygusType()), true);
// get types
Assert(dt[arg].getNumArgs() == 2);
TypeNode tn1 = tds->getArgType(dt[arg], 0);
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
TypeNode btn = TypeNode::fromType(dt.getSygusType());
// for constant reconstruction
- Kind ck = tds->getComparisonKind(btn);
+ Kind ck = getComparisonKind(btn);
Node z = d_qe->getTermUtil()->getTypeValue(btn, 0);
// iterate over constructors
d_generic_base[tn][c] = gr;
return gr;
}
+
+Node CegSingleInvSol::minimizeBuiltinTerm(Node n)
+{
+ Kind nk = n.getKind();
+ if ((nk != EQUAL && nk != LEQ && nk != LT && nk != GEQ && nk != GT)
+ || !n[0].getType().isReal())
+ {
+ return n;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ bool changed = false;
+ std::vector<Node> mon[2];
+ for (unsigned r = 0; r < 2; r++)
+ {
+ unsigned ro = r == 0 ? 1 : 0;
+ Node c;
+ Node nc;
+ if (n[r].getKind() == PLUS)
+ {
+ for (unsigned i = 0; i < n[r].getNumChildren(); i++)
+ {
+ if (ArithMSum::getMonomial(n[r][i], c, nc)
+ && c.getConst<Rational>().isNegativeOne())
+ {
+ mon[ro].push_back(nc);
+ changed = true;
+ }
+ else
+ {
+ if (!n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero())
+ {
+ mon[r].push_back(n[r][i]);
+ }
+ }
+ }
+ }
+ else
+ {
+ if (ArithMSum::getMonomial(n[r], c, nc)
+ && c.getConst<Rational>().isNegativeOne())
+ {
+ mon[ro].push_back(nc);
+ changed = true;
+ }
+ else
+ {
+ if (!n[r].isConst() || !n[r].getConst<Rational>().isZero())
+ {
+ mon[r].push_back(n[r]);
+ }
+ }
+ }
+ }
+ if (changed)
+ {
+ Node nn[2];
+ for (unsigned r = 0; r < 2; r++)
+ {
+ nn[r] = mon[r].size() == 0
+ ? nm->mkConst(Rational(0))
+ : (mon[r].size() == 1 ? mon[r][0] : nm->mkNode(PLUS, mon[r]));
+ }
+ return nm->mkNode(n.getKind(), nn[0], nn[1]);
+ }
+ return n;
+}
+
+Kind CegSingleInvSol::getComparisonKind(TypeNode tn)
+{
+ if (tn.isInteger() || tn.isReal())
+ {
+ return LT;
+ }
+ else if (tn.isBitVector())
+ {
+ return BITVECTOR_ULT;
+ }
+ return UNDEFINED_KIND;
+}
+
+Kind CegSingleInvSol::getPlusKind(TypeNode tn, bool is_neg)
+{
+ if (tn.isInteger() || tn.isReal())
+ {
+ return is_neg ? MINUS : PLUS;
+ }
+ else if (tn.isBitVector())
+ {
+ return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS;
+ }
+ return UNDEFINED_KIND;
+}
}
}
}
return false;
}
-Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
- if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) &&
- ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
- bool changed = false;
- std::vector< Node > mon[2];
- for( unsigned r=0; r<2; r++ ){
- unsigned ro = r==0 ? 1 : 0;
- Node c;
- Node nc;
- if( n[r].getKind()==PLUS ){
- for( unsigned i=0; i<n[r].getNumChildren(); i++ ){
- if (ArithMSum::getMonomial(n[r][i], c, nc)
- && c.getConst<Rational>().isNegativeOne())
- {
- mon[ro].push_back( nc );
- changed = true;
- }else{
- if( !n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero() ){
- mon[r].push_back( n[r][i] );
- }
- }
- }
- }else{
- if (ArithMSum::getMonomial(n[r], c, nc)
- && c.getConst<Rational>().isNegativeOne())
- {
- mon[ro].push_back( nc );
- changed = true;
- }else{
- if( !n[r].isConst() || !n[r].getConst<Rational>().isZero() ){
- mon[r].push_back( n[r] );
- }
- }
- }
- }
- if( changed ){
- Node nn[2];
- for( unsigned r=0; r<2; r++ ){
- nn[r] = mon[r].size()==0 ? NodeManager::currentNM()->mkConst( Rational(0) ) : ( mon[r].size()==1 ? mon[r][0] : NodeManager::currentNM()->mkNode( PLUS, mon[r] ) );
- }
- return NodeManager::currentNM()->mkNode( n.getKind(), nn[0], nn[1] );
- }
- }
- return n;
-}
-
-Node TermDbSygus::expandBuiltinTerm( Node t ){
- if( t.getKind()==EQUAL ){
- if( t[0].getType().isReal() ){
- return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
- NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
- }else if( t[0].getType().isBoolean() ){
- return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
- NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
- }
- }else if( t.getKind()==ITE && t.getType().isBoolean() ){
- return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
- NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
- }
- return Node::null();
-}
-
-
-Kind TermDbSygus::getComparisonKind( TypeNode tn ) {
- if( tn.isInteger() || tn.isReal() ){
- return LT;
- }else if( tn.isBitVector() ){
- return BITVECTOR_ULT;
- }else{
- return UNDEFINED_KIND;
- }
-}
-
-Kind TermDbSygus::getPlusKind( TypeNode tn, bool is_neg ) {
- if( tn.isInteger() || tn.isReal() ){
- return is_neg ? MINUS : PLUS;
- }else if( tn.isBitVector() ){
- return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS;
- }else{
- return UNDEFINED_KIND;
- }
-}
-
bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
if( visited.find( n )==visited.end() ){
visited[n] = true;
return involvesDivByZero( n, visited );
}
-void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
- size_t pos = 0;
- while((pos = str.find(oldStr, pos)) != std::string::npos){
- str.replace(pos, oldStr.length(), newStr);
- pos += newStr.length();
- }
-}
-
Node TermDbSygus::getAnchor( Node n ) {
if( n.getKind()==APPLY_SELECTOR_TOTAL ){
return getAnchor( n[0] );
projects / cvc5.git / commitdiff