Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/theory_uf_model.cpp	Lines:	74	128	57.8 %
Date:	2021-09-16	Branches:	142	440	32.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of Theory UF Model.
 */

#include "theory/uf/theory_uf_model.h"

#include <stack>

#include "expr/attribute.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace uf {

//clear
void UfModelTreeNode::clear(){
  d_data.clear();
  d_value = Node::null();
}

//set value function
void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
  if( d_data.empty() ){
    //overwrite value if either at leaf or this is a fresh tree
    d_value = v;
  }else if( !d_value.isNull() && d_value!=v ){
    //value is no longer constant
    d_value = Node::null();
  }
  if( argIndex<(int)indexOrder.size() ){
    //take r = null when argument is the model basis
    Node r;
    if (ground
        || (!n.isNull()
            && !quantifiers::FirstOrderModel::isModelBasis(
                   n[indexOrder[argIndex]])))
    {
      r = m->getRepresentative( n[ indexOrder[argIndex] ] );
    }
    d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );
  }
}

Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) {
  if(!d_data.empty()) {
    Node defaultValue = argDefaultValue;
    if(d_data.find(Node::null()) != d_data.end()) {
      defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify);
    }

    std::vector<Node> caseArgs;
    std::map<Node, Node> caseValues;

    for (std::pair<const Node, UfModelTreeNode>& p : d_data)
    {
      if (!p.first.isNull())
      {
        Node val =
            p.second.getFunctionValue(args, index + 1, defaultValue, simplify);
        caseArgs.push_back(p.first);
        caseValues[p.first] = val;
      }
    }

    NodeManager* nm = NodeManager::currentNM();
    Node retNode = defaultValue;

    if(!simplify) {
      // "non-simplifying" mode - expand function values to things like:
      //   IF      (x=0 AND y=0 AND z=0) THEN value1
      //   ELSE IF (x=0 AND y=0 AND z=1) THEN value2
      //   [...etc...]
      for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
        Node val = caseValues[ caseArgs[ i ] ];
        if(val.getKind() == ITE) {
          // use a stack to reverse the order, since we're traversing outside-in
          std::stack<TNode> stk;
          do {
            stk.push(val);
            val = val[2];
          } while(val.getKind() == ITE);
          AlwaysAssert(val == defaultValue)
              << "default values don't match when constructing function "
                 "definition!";
          while(!stk.empty()) {
            val = stk.top();
            stk.pop();
            retNode = nm->mkNode(ITE, nm->mkNode(AND, args[index].eqNode(caseArgs[i]), val[0]), val[1], retNode);
          }
        } else {
          retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
        }
      }
    } else {
      // "simplifying" mode - condense function values
      for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
        retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
      }
    }
    return retNode;
  } else {
    Assert(!d_value.isNull());
    return d_value;
  }
}

//update function
void UfModelTreeNode::update( TheoryModel* m ){
  if( !d_value.isNull() ){
    d_value = m->getRepresentative( d_value );
  }
  std::map< Node, UfModelTreeNode > old = d_data;
  d_data.clear();
  for( std::map< Node, UfModelTreeNode >::iterator it = old.begin(); it != old.end(); ++it ){
    Node rep = m->getRepresentative( it->first );
    d_data[ rep ] = it->second;
    d_data[ rep ].update( m );
  }
}

//simplify function
void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){
  if( argIndex<(int)op.getType().getNumChildren()-1 ){
    std::vector< Node > eraseData;
    //first process the default argument
    Node r;
    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
    if( it!=d_data.end() ){
      if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
        eraseData.push_back( r );
      }else{
        it->second.simplify( op, defaultVal, argIndex+1 );
        if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
          defaultVal = it->second.d_value;
        }else{
          defaultVal = Node::null();
          if( it->second.isEmpty() ){
            eraseData.push_back( r );
          }
        }
      }
    }
    //now see if any children can be removed, and simplify the ones that cannot
    for (auto& kv : d_data)
    {
      if (!kv.first.isNull())
      {
        if (!defaultVal.isNull() && kv.second.d_value == defaultVal)
        {
          eraseData.push_back(kv.first);
        }
        else
        {
          kv.second.simplify(op, defaultVal, argIndex + 1);
          if (kv.second.isEmpty())
          {
            eraseData.push_back(kv.first);
          }
        }
      }
    }
    for( int i=0; i<(int)eraseData.size(); i++ ){
      d_data.erase( eraseData[i] );
    }
  }
}

//is total function
bool UfModelTreeNode::isTotal( Node op, int argIndex ){
  if( argIndex==(int)(op.getType().getNumChildren()-1) ){
    return !d_value.isNull();
  }else{
    Node r;
    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
    if( it!=d_data.end() ){
      return it->second.isTotal( op, argIndex+1 );
    }else{
      return false;
    }
  }
}

void indent( std::ostream& out, int ind ){
  for( int i=0; i<ind; i++ ){
    out << " ";
  }
}

void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
  if( !d_data.empty() ){
    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
      if( !it->first.isNull() ){
        indent( out, ind );
        out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
        it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );
      }
    }
    if( d_data.find( Node::null() )!=d_data.end() ){
      d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );
    }
  }else{
    indent( out, ind );
    out << "return ";
    out << m->getRepresentative(d_value);
    out << std::endl;
  }
}

Node UfModelTree::getFunctionValue( std::vector< Node >& args, bool simplify ){
  Node body = d_tree.getFunctionValue( args, 0, Node::null(), simplify );
  if(simplify) {
    body = Rewriter::rewrite( body );
  }
  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
}

Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
  TypeNode type = d_op.getType();
  std::vector< Node > vars;
  for( size_t i=0; i<type.getNumChildren()-1; i++ ){
    std::stringstream ss;
    ss << argPrefix << (i+1);
    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
  }
  return getFunctionValue( vars, simplify );
}

}  // namespace uf
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of Theory UF Model.
14		*/
15
16		#include "theory/uf/theory_uf_model.h"
17
18		#include <stack>
19
20		#include "expr/attribute.h"
21		#include "theory/quantifiers/first_order_model.h"
22		#include "theory/rewriter.h"
23		#include "theory/theory_model.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace uf {
30
31		//clear
32		void UfModelTreeNode::clear(){
33		d_data.clear();
34		d_value = Node::null();
35		}
36
37		//set value function
38	148044	void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
39	148044	if( d_data.empty() ){
40		//overwrite value if either at leaf or this is a fresh tree
41	114604	d_value = v;
42	33440	}else if( !d_value.isNull() && d_value!=v ){
43		//value is no longer constant
44	2879	d_value = Node::null();
45		}
46	148044	if( argIndex<(int)indexOrder.size() ){
47		//take r = null when argument is the model basis
48	246480	Node r;
49	123240	if (ground
50	207886	\|\| (!n.isNull()
51	123240	&& !quantifiers::FirstOrderModel::isModelBasis(
52		n[indexOrder[argIndex]])))
53		{
54	84646	r = m->getRepresentative( n[ indexOrder[argIndex] ] );
55		}
56	123240	d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );
57		}
58	148044	}
59
60	56541	Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) {
61	56541	if(!d_data.empty()) {
62	91920	Node defaultValue = argDefaultValue;
63	45960	if(d_data.find(Node::null()) != d_data.end()) {
64	38594	defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify);
65		}
66
67	91920	std::vector<Node> caseArgs;
68	91920	std::map<Node, Node> caseValues;
69
70	98016	for (std::pair<const Node, UfModelTreeNode>& p : d_data)
71		{
72	52056	if (!p.first.isNull())
73		{
74		Node val =
75	26924	p.second.getFunctionValue(args, index + 1, defaultValue, simplify);
76	13462	caseArgs.push_back(p.first);
77	13462	caseValues[p.first] = val;
78		}
79		}
80
81	45960	NodeManager* nm = NodeManager::currentNM();
82	91920	Node retNode = defaultValue;
83
84	45960	if(!simplify) {
85		// "non-simplifying" mode - expand function values to things like:
86		// IF (x=0 AND y=0 AND z=0) THEN value1
87		// ELSE IF (x=0 AND y=0 AND z=1) THEN value2
88		// [...etc...]
89		for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
90		Node val = caseValues[ caseArgs[ i ] ];
91		if(val.getKind() == ITE) {
92		// use a stack to reverse the order, since we're traversing outside-in
93		std::stack<TNode> stk;
94		do {
95		stk.push(val);
96		val = val[2];
97		} while(val.getKind() == ITE);
98		AlwaysAssert(val == defaultValue)
99		<< "default values don't match when constructing function "
100		"definition!";
101		while(!stk.empty()) {
102		val = stk.top();
103		stk.pop();
104		retNode = nm->mkNode(ITE, nm->mkNode(AND, args[index].eqNode(caseArgs[i]), val[0]), val[1], retNode);
105		}
106		} else {
107		retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
108		}
109		}
110		} else {
111		// "simplifying" mode - condense function values
112	59422	for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
113	13462	retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
114		}
115		}
116	45960	return retNode;
117		} else {
118	10581	Assert(!d_value.isNull());
119	10581	return d_value;
120		}
121		}
122
123		//update function
124		void UfModelTreeNode::update( TheoryModel* m ){
125		if( !d_value.isNull() ){
126		d_value = m->getRepresentative( d_value );
127		}
128		std::map< Node, UfModelTreeNode > old = d_data;
129		d_data.clear();
130		for( std::map< Node, UfModelTreeNode >::iterator it = old.begin(); it != old.end(); ++it ){
131		Node rep = m->getRepresentative( it->first );
132		d_data[ rep ] = it->second;
133		d_data[ rep ].update( m );
134		}
135		}
136
137		//simplify function
138	56541	void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){
139	56541	if( argIndex<(int)op.getType().getNumChildren()-1 ){
140	91920	std::vector< Node > eraseData;
141		//first process the default argument
142	91920	Node r;
143	45960	std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
144	45960	if( it!=d_data.end() ){
145	38594	if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
146		eraseData.push_back( r );
147		}else{
148	38594	it->second.simplify( op, defaultVal, argIndex+1 );
149	38594	if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
150	38594	defaultVal = it->second.d_value;
151		}else{
152		defaultVal = Node::null();
153		if( it->second.isEmpty() ){
154		eraseData.push_back( r );
155		}
156		}
157		}
158		}
159		//now see if any children can be removed, and simplify the ones that cannot
160	104793	for (auto& kv : d_data)
161		{
162	58833	if (!kv.first.isNull())
163		{
164	20239	if (!defaultVal.isNull() && kv.second.d_value == defaultVal)
165		{
166	6777	eraseData.push_back(kv.first);
167		}
168		else
169		{
170	13462	kv.second.simplify(op, defaultVal, argIndex + 1);
171	13462	if (kv.second.isEmpty())
172		{
173		eraseData.push_back(kv.first);
174		}
175		}
176		}
177		}
178	52737	for( int i=0; i<(int)eraseData.size(); i++ ){
179	6777	d_data.erase( eraseData[i] );
180		}
181		}
182	56541	}
183
184		//is total function
185	2893826	bool UfModelTreeNode::isTotal( Node op, int argIndex ){
186	2893826	if( argIndex==(int)(op.getType().getNumChildren()-1) ){
187	38594	return !d_value.isNull();
188		}else{
189	5710464	Node r;
190	2855232	std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
191	2855232	if( it!=d_data.end() ){
192	2855232	return it->second.isTotal( op, argIndex+1 );
193		}else{
194		return false;
195		}
196		}
197		}
198
199		void indent( std::ostream& out, int ind ){
200		for( int i=0; i<ind; i++ ){
201		out << " ";
202		}
203		}
204
205		void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
206		if( !d_data.empty() ){
207		for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
208		if( !it->first.isNull() ){
209		indent( out, ind );
210		out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
211		it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );
212		}
213		}
214		if( d_data.find( Node::null() )!=d_data.end() ){
215		d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );
216		}
217		}else{
218		indent( out, ind );
219		out << "return ";
220		out << m->getRepresentative(d_value);
221		out << std::endl;
222		}
223		}
224
225	4485	Node UfModelTree::getFunctionValue( std::vector< Node >& args, bool simplify ){
226	8970	Node body = d_tree.getFunctionValue( args, 0, Node::null(), simplify );
227	4485	if(simplify) {
228	4485	body = Rewriter::rewrite( body );
229		}
230	8970	Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
231	8970	return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
232		}
233
234	4485	Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
235	8970	TypeNode type = d_op.getType();
236	8970	std::vector< Node > vars;
237	43079	for( size_t i=0; i<type.getNumChildren()-1; i++ ){
238	77188	std::stringstream ss;
239	38594	ss << argPrefix << (i+1);
240	38594	vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
241		}
242	8970	return getFunctionValue( vars, simplify );
243		}
244
245		} // namespace uf
246		} // namespace theory
247	29577	} // namespace cvc5