summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/passes/nl_ext_purify.cpp130
-rw-r--r--src/preprocessing/passes/nl_ext_purify.h57
-rw-r--r--src/preprocessing/passes/quantifier_macros.cpp550
-rw-r--r--src/preprocessing/passes/quantifier_macros.h89
-rw-r--r--src/preprocessing/passes/unconstrained_simplifier.cpp847
-rw-r--r--src/preprocessing/passes/unconstrained_simplifier.h75
-rw-r--r--src/preprocessing/preprocessing_pass.h1
-rw-r--r--src/preprocessing/preprocessing_pass_context.h3
8 files changed, 1752 insertions, 0 deletions
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
new file mode 100644
index 000000000..afb092571
--- /dev/null
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -0,0 +1,130 @@
+/********************* */
+/*! \file nl_ext_purify.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief The NlExtPurify preprocessing pass
+ **
+ ** Purifies non-linear terms
+ **/
+
+#include "preprocessing/passes/nl_ext_purify.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+Node NlExtPurify::purifyNlTerms(TNode n,
+ NodeMap& cache,
+ NodeMap& bcache,
+ std::vector<Node>& var_eq,
+ bool beneathMult)
+{
+ if (beneathMult)
+ {
+ NodeMap::iterator find = bcache.find(n);
+ if (find != bcache.end())
+ {
+ return (*find).second;
+ }
+ }
+ else
+ {
+ NodeMap::iterator find = cache.find(n);
+ if (find != cache.end())
+ {
+ return (*find).second;
+ }
+ }
+ Node ret = n;
+ if (n.getNumChildren() > 0)
+ {
+ if (beneathMult
+ && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
+ {
+ // don't do it if it rewrites to a constant
+ Node nr = Rewriter::rewrite(n);
+ if (nr.isConst())
+ {
+ // return the rewritten constant
+ ret = nr;
+ }
+ else
+ {
+ // new variable
+ ret = NodeManager::currentNM()->mkSkolem(
+ "__purifyNl_var",
+ n.getType(),
+ "Variable introduced in purifyNl pass");
+ Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
+ var_eq.push_back(np.eqNode(ret));
+ Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np
+ << std::endl;
+ }
+ }
+ else
+ {
+ bool beneathMultNew = beneathMult || n.getKind() == kind::MULT;
+ bool childChanged = false;
+ std::vector<Node> children;
+ for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i)
+ {
+ Node nc = purifyNlTerms(n[i], cache, bcache, var_eq, beneathMultNew);
+ childChanged = childChanged || nc != n[i];
+ children.push_back(nc);
+ }
+ if (childChanged)
+ {
+ ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+ }
+ }
+ }
+ if (beneathMult)
+ {
+ bcache[n] = ret;
+ }
+ else
+ {
+ cache[n] = ret;
+ }
+ return ret;
+}
+
+NlExtPurify::NlExtPurify(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "nl-ext-purify"){};
+
+PreprocessingPassResult NlExtPurify::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ unordered_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> bcache;
+ std::vector<Node> var_eq;
+ unsigned size = assertionsToPreprocess->size();
+ for (unsigned i = 0; i < size; ++i)
+ {
+ Node a = (*assertionsToPreprocess)[i];
+ assertionsToPreprocess->replace(i, purifyNlTerms(a, cache, bcache, var_eq));
+ Trace("nl-ext-purify") << "Purify : " << a << " -> "
+ << (*assertionsToPreprocess)[i] << "\n";
+ }
+ if (!var_eq.empty())
+ {
+ unsigned lastIndex = size - 1;
+ var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]);
+ assertionsToPreprocess->replace(
+ lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq));
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h
new file mode 100644
index 000000000..8d28b0742
--- /dev/null
+++ b/src/preprocessing/passes/nl_ext_purify.h
@@ -0,0 +1,57 @@
+/********************* */
+/*! \file nl_ext_purify.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief The NlExtPurify preprocessing pass
+ **
+ ** Purifies non-linear terms by replacing sums under multiplications by fresh
+ ** variables
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+#define __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+
+class NlExtPurify : public PreprocessingPass
+{
+ public:
+ NlExtPurify(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ Node purifyNlTerms(TNode n,
+ NodeMap& cache,
+ NodeMap& bcache,
+ std::vector<Node>& var_eq,
+ bool beneathMult = false);
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
new file mode 100644
index 000000000..e3bc02309
--- /dev/null
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -0,0 +1,550 @@
+/********************* */
+/*! \file quantifier_macros.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King, Kshitij Bansal
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Sort inference module
+ **
+ ** This class implements quantifiers macro definitions.
+ **/
+
+#include "preprocessing/passes/quantifier_macros.h"
+
+#include <vector>
+
+#include "options/quantifiers_modes.h"
+#include "options/quantifiers_options.h"
+#include "proof/proof_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
+
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+QuantifierMacros::QuantifierMacros(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "quantifier-macros"),
+ d_ground_macros(false)
+{
+}
+
+PreprocessingPassResult QuantifierMacros::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ bool success;
+ do
+ {
+ success = simplify(assertionsToPreprocess->ref(), true);
+ } while (success);
+ finalizeDefinitions();
+ clearMaps();
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+void QuantifierMacros::clearMaps()
+{
+ d_macro_basis.clear();
+ d_macro_defs.clear();
+ d_macro_defs_new.clear();
+ d_macro_def_contains.clear();
+ d_simplify_cache.clear();
+ d_quant_macros.clear();
+ d_ground_macros = false;
+}
+
+bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
+ unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1;
+ for( unsigned r=0; r<rmax; r++ ){
+ d_ground_macros = (r==0);
+ Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
+ //first, collect macro definitions
+ std::vector< Node > macro_assertions;
+ for( int i=0; i<(int)assertions.size(); i++ ){
+ Trace("macros-debug") << " process assertion " << assertions[i] << std::endl;
+ if( processAssertion( assertions[i] ) ){
+ PROOF(
+ if( std::find( macro_assertions.begin(), macro_assertions.end(), assertions[i] )==macro_assertions.end() ){
+ macro_assertions.push_back( assertions[i] );
+ }
+ );
+ //process this assertion again
+ i--;
+ }
+ }
+ Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl;
+ if( doRewrite && !d_macro_defs_new.empty() ){
+ bool retVal = false;
+ Trace("macros") << "Do simplifications..." << std::endl;
+ //now, rewrite based on macro definitions
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ Node curr = simplify( assertions[i] );
+ if( curr!=assertions[i] ){
+ curr = Rewriter::rewrite( curr );
+ Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
+ //for now, it is dependent upon all assertions involving macros, this is an over-approximation.
+ //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula,
+ // which is expensive.
+ PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]);
+ for (unsigned j = 0; j < macro_assertions.size(); j++) {
+ if (macro_assertions[j] != assertions[i])
+ {
+ ProofManager::currentPM()->addDependence(
+ curr, macro_assertions[j]);
+ }
+ });
+ assertions[i] = curr;
+ retVal = true;
+ }
+ }
+ d_macro_defs_new.clear();
+ if( retVal ){
+ return true;
+ }
+ }
+ }
+ if( Trace.isOn("macros-warn") ){
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ debugMacroDefinition( assertions[i], assertions[i] );
+ }
+ }
+ return false;
+}
+
+bool QuantifierMacros::processAssertion( Node n ) {
+ if( n.getKind()==AND ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( processAssertion( n[i] ) ){
+ return true;
+ }
+ }
+ }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){
+ std::vector< Node > args;
+ for( size_t j=0; j<n[0].getNumChildren(); j++ ){
+ args.push_back( n[0][j] );
+ }
+ Node nproc = n[1];
+ if( !d_macro_defs_new.empty() ){
+ nproc = simplify( nproc );
+ if( nproc!=n[1] ){
+ nproc = Rewriter::rewrite( nproc );
+ }
+ }
+ //look at the body of the quantifier for macro definition
+ if( process( nproc, true, args, n ) ){
+ d_quant_macros[n] = true;
+ return true;
+ }
+ }
+ return false;
+}
+
+bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==APPLY_UF ){
+ Node nop = n.getOperator();
+ if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){
+ return true;
+ }
+ if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
+ opc.push_back( nop );
+ }
+ }else if( d_ground_macros && n.getKind()==FORALL ){
+ return true;
+ }
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ if( containsBadOp( n[i], op, opc, visited ) ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
+ return pol && n.getKind()==EQUAL;
+}
+
+bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
+ Node icn = d_preprocContext->getTheoryEngine()
+ ->getQuantifiersEngine()
+ ->getTermUtil()
+ ->substituteBoundVariablesToInstConstants(n, f);
+ Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
+ std::vector< Node > var;
+ quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var);
+ Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
+ std::vector< Node > trigger_var;
+ inst::Trigger::getTriggerVariables( icn, f, trigger_var );
+ Trace("macros-debug2") << "Done." << std::endl;
+ //only if all variables are also trigger variables
+ return trigger_var.size()>=var.size();
+}
+
+bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
+ Assert( n.getKind()==APPLY_UF );
+ TypeNode tno = n.getOperator().getType();
+ std::map< Node, bool > vars;
+ // allow if a vector of unique variables of the same type as UF arguments
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()!=BOUND_VARIABLE ){
+ return false;
+ }
+ if( n[i].getType()!=tno[i] ){
+ return false;
+ }
+ if( vars.find( n[i] )==vars.end() ){
+ vars[n[i]] = true;
+ }else{
+ return false;
+ }
+ }
+ return true;
+}
+
+void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==APPLY_UF ){
+ if( isBoundVarApplyUf( n ) ){
+ candidates.push_back( n );
+ }
+ }else if( n.getKind()==PLUS ){
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ getMacroCandidates( n[i], candidates, visited );
+ }
+ }else if( n.getKind()==MULT ){
+ //if the LHS is a constant
+ if( n.getNumChildren()==2 && n[0].isConst() ){
+ getMacroCandidates( n[1], candidates, visited );
+ }
+ }else if( n.getKind()==NOT ){
+ getMacroCandidates( n[0], candidates, visited );
+ }
+ }
+}
+
+Node QuantifierMacros::solveInEquality( Node n, Node lit ){
+ if( lit.getKind()==EQUAL ){
+ //return the opposite side of the equality if defined that way
+ for( int i=0; i<2; i++ ){
+ if( lit[i]==n ){
+ return lit[i==0 ? 1 : 0];
+ }else if( lit[i].getKind()==NOT && lit[i][0]==n ){
+ return lit[i==0 ? 1 : 0].negate();
+ }
+ }
+ std::map<Node, Node> msum;
+ if (ArithMSum::getMonomialSumLit(lit, msum))
+ {
+ Node veq_c;
+ Node val;
+ int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL);
+ if (res != 0 && veq_c.isNull())
+ {
+ return val;
+ }
+ }
+ }
+ Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;
+ return Node::null();
+}
+
+bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
+ if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
+ if( retOnly ){
+ return true;
+ }else{
+ vars.push_back( n );
+ }
+ }
+ }
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
+ std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){
+ bool success = true;
+ for( size_t a=0; a<v_quant.size(); a++ ){
+ if( !solved[ v_quant[a] ].isNull() ){
+ vars.push_back( v_quant[a] );
+ subs.push_back( solved[ v_quant[a] ] );
+ }else{
+ if( reqComplete ){
+ success = false;
+ break;
+ }
+ }
+ }
+ return success;
+}
+
+bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
+ Trace("macros-debug") << " process " << n << std::endl;
+ if( n.getKind()==NOT ){
+ return process( n[0], !pol, args, f );
+ }else if( n.getKind()==AND || n.getKind()==OR ){
+ //bool favorPol = (n.getKind()==AND)==pol;
+ //conditional?
+ }else if( n.getKind()==ITE ){
+ //can not do anything
+ }else if( n.getKind()==APPLY_UF ){
+ //predicate case
+ if( isBoundVarApplyUf( n ) ){
+ Node op = n.getOperator();
+ if( d_macro_defs.find( op )==d_macro_defs.end() ){
+ Node n_def = NodeManager::currentNM()->mkConst( pol );
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ std::stringstream ss;
+ ss << "mda_" << op << "";
+ Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" );
+ d_macro_basis[op].push_back( v );
+ }
+ //contains no ops
+ std::vector< Node > op_contains;
+ //add the macro
+ addMacro( op, n_def, op_contains );
+ return true;
+ }
+ }
+ }else{
+ //literal case
+ if( isMacroLiteral( n, pol ) ){
+ Trace("macros-debug") << "Check macro literal : " << n << std::endl;
+ std::map< Node, bool > visited;
+ std::vector< Node > candidates;
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ getMacroCandidates( n[i], candidates, visited );
+ }
+ for( size_t i=0; i<candidates.size(); i++ ){
+ Node m = candidates[i];
+ Node op = m.getOperator();
+ Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
+ if( d_macro_defs.find( op )==d_macro_defs.end() ){
+ std::vector< Node > fvs;
+ visited.clear();
+ getFreeVariables( m, args, fvs, false, visited );
+ //get definition and condition
+ Node n_def = solveInEquality( m, n ); //definition for the macro
+ if( !n_def.isNull() ){
+ Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
+ Trace("macros-debug") << " corresponding definition is : " << n_def << std::endl;
+ visited.clear();
+ //definition must exist and not contain any free variables apart from fvs
+ if( !getFreeVariables( n_def, args, fvs, true, visited ) ){
+ Trace("macros-debug") << "...free variables are contained." << std::endl;
+ visited.clear();
+ //cannot contain a defined operator, opc is list of functions it contains
+ std::vector< Node > opc;
+ if( !containsBadOp( n_def, op, opc, visited ) ){
+ Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl;
+ //must be ground UF term if mode is GROUND_UF
+ if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){
+ Trace("macros-debug") << "...respects ground-uf constraint." << std::endl;
+ //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
+ // x1 ... xn are distinct variables
+ if( d_macro_basis[op].empty() ){
+ for( size_t a=0; a<m.getNumChildren(); a++ ){
+ std::stringstream ss;
+ ss << "mda_" << op << "";
+ Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
+ d_macro_basis[op].push_back( v );
+ }
+ }
+ std::map< Node, Node > solved;
+ for( size_t a=0; a<m.getNumChildren(); a++ ){
+ solved[m[a]] = d_macro_basis[op][a];
+ }
+ std::vector< Node > vars;
+ std::vector< Node > subs;
+ if( getSubstitution( fvs, solved, vars, subs, true ) ){
+ n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ addMacro( op, n_def, opc );
+ return true;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ return false;
+}
+
+Node QuantifierMacros::simplify( Node n ){
+ if( n.getNumChildren()==0 ){
+ return n;
+ }else{
+ std::map< Node, Node >::iterator itn = d_simplify_cache.find( n );
+ if( itn!=d_simplify_cache.end() ){
+ return itn->second;
+ }else{
+ Node ret = n;
+ Trace("macros-debug") << " simplify " << n << std::endl;
+ std::vector< Node > children;
+ bool childChanged = false;
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ Node nn = simplify( n[i] );
+ children.push_back( nn );
+ childChanged = childChanged || nn!=n[i];
+ }
+ bool retSet = false;
+ if( n.getKind()==APPLY_UF ){
+ Node op = n.getOperator();
+ std::map< Node, Node >::iterator it = d_macro_defs.find( op );
+ if( it!=d_macro_defs.end() && !it->second.isNull() ){
+ //only apply if children are subtypes of arguments
+ bool success = true;
+ // FIXME : this can be eliminated when we have proper typing rules
+ std::vector< Node > cond;
+ TypeNode tno = op.getType();
+ for( unsigned i=0; i<children.size(); i++ ){
+ Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] );
+ if( etc.isNull() ){
+ //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op,
+ // and not ensuring it applies to n when its types are correct.
+ //Assert( false );
+ success = false;
+ break;
+ }else if( !etc.isConst() ){
+ cond.push_back( etc );
+ }
+ Assert( children[i].getType().isSubtypeOf( tno[i] ) );
+ }
+ if( success ){
+ //do substitution if necessary
+ ret = it->second;
+ std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
+ if( itb!=d_macro_basis.end() ){
+ ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
+ }
+ if( !cond.empty() ){
+ Node cc = cond.size()==1 ? cond[0] : NodeManager::currentNM()->mkNode( kind::AND, cond );
+ ret = NodeManager::currentNM()->mkNode( kind::ITE, cc, ret, n );
+ }
+ retSet = true;
+ }
+ }
+ }
+ if( !retSet && childChanged ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), n.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ d_simplify_cache[n] = ret;
+ return ret;
+ }
+ }
+}
+
+void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) {
+ //for debugging, ensure that all previous definitions have been eliminated
+ if( n.getKind()==APPLY_UF ){
+ Node op = n.getOperator();
+ if( d_macro_defs.find( op )!=d_macro_defs.end() ){
+ if( d_macro_defs.find( oo )!=d_macro_defs.end() ){
+ Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl;
+ }else{
+ Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl;
+ }
+ Trace("macros-warn") << " contains defined function " << op << "!!!" << std::endl;
+ }
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ debugMacroDefinition( oo, n[i] );
+ }
+}
+
+void QuantifierMacros::finalizeDefinitions() {
+ bool doDefs = false;
+ if( Trace.isOn("macros-warn") ){
+ doDefs = true;
+ }
+ if( options::incrementalSolving() || options::produceModels() || doDefs ){
+ Trace("macros") << "Store as defined functions..." << std::endl;
+ //also store as defined functions
+ for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
+ Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
+ Trace("macros-def") << " basis is : ";
+ std::vector< Node > nargs;
+ std::vector< Expr > args;
+ for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
+ Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
+ Trace("macros-def") << d_macro_basis[it->first][i] << " ";
+ nargs.push_back( bv );
+ args.push_back( bv.toExpr() );
+ }
+ Trace("macros-def") << std::endl;
+ Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
+ smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+
+ if( Trace.isOn("macros-warn") ){
+ debugMacroDefinition( it->first, sbody );
+ }
+ }
+ Trace("macros") << "done." << std::endl;
+ }
+}
+
+void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
+ Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl;
+ d_simplify_cache.clear();
+ d_macro_defs[op] = n;
+ d_macro_defs_new[op] = n;
+ //substitute into all previous
+ std::vector< Node > dep_ops;
+ dep_ops.push_back( op );
+ Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl;
+ for( unsigned i=0; i<d_macro_def_contains[op].size(); i++ ){
+ Node cop = d_macro_def_contains[op][i];
+ Node def = d_macro_defs[cop];
+ def = simplify( def );
+ d_macro_defs[cop] = def;
+ if( d_macro_defs_new.find( cop )!=d_macro_defs_new.end() ){
+ d_macro_defs_new[cop] = def;
+ }
+ dep_ops.push_back( cop );
+ }
+ //store the contains op information
+ for( unsigned i=0; i<opc.size(); i++ ){
+ for( unsigned j=0; j<dep_ops.size(); j++ ){
+ Node dop = dep_ops[j];
+ if( std::find( d_macro_def_contains[opc[i]].begin(), d_macro_def_contains[opc[i]].end(), dop )==d_macro_def_contains[opc[i]].end() ){
+ d_macro_def_contains[opc[i]].push_back( dop );
+ }
+ }
+ }
+}
+
+} // passes
+} // preprocessing
+} // CVC4
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
new file mode 100644
index 000000000..092a62942
--- /dev/null
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -0,0 +1,89 @@
+/********************* */
+/*! \file quantifier_macros.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Pre-process step for detecting quantifier macro definitions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class QuantifierMacros : public PreprocessingPass
+{
+ public:
+ QuantifierMacros(PreprocessingPassContext* preprocContext);
+ ~QuantifierMacros() {}
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ bool processAssertion(Node n);
+ bool isBoundVarApplyUf(Node n);
+ bool process(Node n, bool pol, std::vector<Node>& args, Node f);
+ bool containsBadOp(Node n,
+ Node op,
+ std::vector<Node>& opc,
+ std::map<Node, bool>& visited);
+ bool isMacroLiteral(Node n, bool pol);
+ bool isGroundUfTerm(Node f, Node n);
+ void getMacroCandidates(Node n,
+ std::vector<Node>& candidates,
+ std::map<Node, bool>& visited);
+ Node solveInEquality(Node n, Node lit);
+ bool getFreeVariables(Node n,
+ std::vector<Node>& v_quant,
+ std::vector<Node>& vars,
+ bool retOnly,
+ std::map<Node, bool>& visited);
+ bool getSubstitution(std::vector<Node>& v_quant,
+ std::map<Node, Node>& solved,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ bool reqComplete);
+ void addMacro(Node op, Node n, std::vector<Node>& opc);
+ void debugMacroDefinition(Node oo, Node n);
+ bool simplify(std::vector<Node>& assertions, bool doRewrite = false);
+ Node simplify(Node n);
+ void finalizeDefinitions();
+ void clearMaps();
+
+ // map from operators to macro basis terms
+ std::map<Node, std::vector<Node> > d_macro_basis;
+ // map from operators to macro definition
+ std::map<Node, Node> d_macro_defs;
+ std::map<Node, Node> d_macro_defs_new;
+ // operators to macro ops that contain them
+ std::map<Node, std::vector<Node> > d_macro_def_contains;
+ // simplify caches
+ std::map<Node, Node> d_simplify_cache;
+ std::map<Node, bool> d_quant_macros;
+ bool d_ground_macros;
+};
+
+} // passes
+} // preprocessing
+} // CVC4
+
+#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
new file mode 100644
index 000000000..6bb46f3f2
--- /dev/null
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -0,0 +1,847 @@
+/********************* */
+/*! \file unconstrained_simplifier.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Clark Barrett, Tim King, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Simplifications based on unconstrained variables
+ **
+ ** This module implements a preprocessing phase which replaces certain
+ ** "unconstrained" expressions by variables. Based on Roberto
+ ** Bruttomesso's PhD thesis.
+ **/
+
+#include "preprocessing/passes/unconstrained_simplifier.h"
+
+#include "smt/smt_statistics_registry.h"
+#include "theory/logic_info.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+UnconstrainedSimplifier::UnconstrainedSimplifier(
+ PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "unconstrained-simplifier"),
+ d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
+ d_context(preprocContext->getDecisionContext()),
+ d_substitutions(preprocContext->getDecisionContext()),
+ d_logicInfo(preprocContext->getLogicInfo())
+{
+ smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim);
+}
+
+UnconstrainedSimplifier::~UnconstrainedSimplifier()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim);
+}
+
+struct unc_preprocess_stack_element
+{
+ TNode node;
+ TNode parent;
+ unc_preprocess_stack_element(TNode n) : node(n) {}
+ unc_preprocess_stack_element(TNode n, TNode p) : node(n), parent(p) {}
+}; /* struct unc_preprocess_stack_element */
+
+void UnconstrainedSimplifier::visitAll(TNode assertion)
+{
+ // Do a topological sort of the subexpressions and substitute them
+ vector<unc_preprocess_stack_element> toVisit;
+ toVisit.push_back(assertion);
+
+ while (!toVisit.empty())
+ {
+ // The current node we are processing
+ TNode current = toVisit.back().node;
+ TNode parent = toVisit.back().parent;
+ toVisit.pop_back();
+
+ TNodeCountMap::iterator find = d_visited.find(current);
+ if (find != d_visited.end())
+ {
+ if (find->second == 1)
+ {
+ d_visitedOnce.erase(current);
+ if (current.isVar())
+ {
+ d_unconstrained.erase(current);
+ }
+ }
+ ++find->second;
+ continue;
+ }
+
+ d_visited[current] = 1;
+ d_visitedOnce[current] = parent;
+
+ if (current.getNumChildren() == 0)
+ {
+ if (current.getKind() == kind::VARIABLE
+ || current.getKind() == kind::SKOLEM)
+ {
+ d_unconstrained.insert(current);
+ }
+ }
+ else
+ {
+ for (TNode childNode : current)
+ {
+ toVisit.push_back(unc_preprocess_stack_element(childNode, current));
+ }
+ }
+ }
+}
+
+Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
+{
+ Node n = NodeManager::currentNM()->mkSkolem(
+ "unconstrained",
+ t,
+ "a new var introduced because of unconstrained variable "
+ + var.toString());
+ return n;
+}
+
+void UnconstrainedSimplifier::processUnconstrained()
+{
+ NodeManager* nm = NodeManager::currentNM();
+
+ vector<TNode> workList(d_unconstrained.begin(), d_unconstrained.end());
+ Node currentSub;
+ TNode parent;
+ bool swap;
+ bool isSigned;
+ bool strict;
+ vector<TNode> delayQueueLeft;
+ vector<Node> delayQueueRight;
+
+ TNode current = workList.back();
+ workList.pop_back();
+ for (;;)
+ {
+ Assert(d_visitedOnce.find(current) != d_visitedOnce.end());
+ parent = d_visitedOnce[current];
+ if (!parent.isNull())
+ {
+ swap = isSigned = strict = false;
+ bool checkParent = false;
+ switch (parent.getKind())
+ {
+ // If-then-else operator - any two unconstrained children makes the
+ // parent unconstrained
+ case kind::ITE:
+ {
+ Assert(parent[0] == current || parent[1] == current
+ || parent[2] == current);
+ bool uCond =
+ parent[0] == current
+ || d_unconstrained.find(parent[0]) != d_unconstrained.end();
+ bool uThen =
+ parent[1] == current
+ || d_unconstrained.find(parent[1]) != d_unconstrained.end();
+ bool uElse =
+ parent[2] == current
+ || d_unconstrained.find(parent[2]) != d_unconstrained.end();
+ if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse))
+ {
+ if (d_unconstrained.find(parent) == d_unconstrained.end()
+ && !d_substitutions.hasSubstitution(parent))
+ {
+ ++d_numUnconstrainedElim;
+ if (uThen)
+ {
+ if (parent[1] != current)
+ {
+ if (parent[1].isVar())
+ {
+ currentSub = parent[1];
+ }
+ else
+ {
+ Assert(d_substitutions.hasSubstitution(parent[1]));
+ currentSub = d_substitutions.apply(parent[1]);
+ }
+ }
+ else if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ }
+ else if (parent[2] != current)
+ {
+ if (parent[2].isVar())
+ {
+ currentSub = parent[2];
+ }
+ else
+ {
+ Assert(d_substitutions.hasSubstitution(parent[2]));
+ currentSub = d_substitutions.apply(parent[2]);
+ }
+ }
+ else if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ current = parent;
+ }
+ else
+ {
+ currentSub = Node();
+ }
+ }
+ else if (uCond)
+ {
+ Cardinality card = parent.getType().getCardinality();
+ if (card.isFinite() && !card.isLargeFinite()
+ && card.getFiniteCardinality() == 2)
+ {
+ // Special case: condition is unconstrained, then and else are
+ // different, and total cardinality of the type is 2, then the
+ // result is unconstrained
+ Node test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
+ if (test == nm->mkConst<bool>(false))
+ {
+ ++d_numUnconstrainedElim;
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ currentSub = newUnconstrainedVar(parent.getType(), currentSub);
+ current = parent;
+ }
+ }
+ }
+ break;
+ }
+
+ // Comparisons that return a different type - assuming domains are
+ // larger than 1, any unconstrained child makes parent unconstrained as
+ // well
+ case kind::EQUAL:
+ if (parent[0].getType() != parent[1].getType())
+ {
+ TNode other = (parent[0] == current) ? parent[1] : parent[0];
+ if (current.getType().isSubtypeOf(other.getType()))
+ {
+ break;
+ }
+ }
+ if (parent[0].getType().isDatatype())
+ {
+ TypeNode tn = parent[0].getType();
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ if (dt.isRecursiveSingleton(tn.toType()))
+ {
+ // domain size may be 1
+ break;
+ }
+ }
+ if (parent[0].getType().isBoolean())
+ {
+ checkParent = true;
+ break;
+ }
+ case kind::BITVECTOR_COMP:
+ case kind::LT:
+ case kind::LEQ:
+ case kind::GT:
+ case kind::GEQ:
+ {
+ if (d_unconstrained.find(parent) == d_unconstrained.end()
+ && !d_substitutions.hasSubstitution(parent))
+ {
+ ++d_numUnconstrainedElim;
+ Assert(parent[0] != parent[1]
+ && (parent[0] == current || parent[1] == current));
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ currentSub = newUnconstrainedVar(parent.getType(), currentSub);
+ current = parent;
+ }
+ else
+ {
+ currentSub = Node();
+ }
+ break;
+ }
+
+ // Unary operators that propagate unconstrainedness
+ case kind::NOT:
+ case kind::BITVECTOR_NOT:
+ case kind::BITVECTOR_NEG:
+ case kind::UMINUS:
+ ++d_numUnconstrainedElim;
+ Assert(parent[0] == current);
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ current = parent;
+ break;
+
+ // Unary operators that propagate unconstrainedness and return a
+ // different type
+ case kind::BITVECTOR_EXTRACT:
+ ++d_numUnconstrainedElim;
+ Assert(parent[0] == current);
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ currentSub = newUnconstrainedVar(parent.getType(), currentSub);
+ current = parent;
+ break;
+
+ // Operators returning same type requiring all children to be
+ // unconstrained
+ case kind::AND:
+ case kind::OR:
+ case kind::IMPLIES:
+ case kind::BITVECTOR_AND:
+ case kind::BITVECTOR_OR:
+ case kind::BITVECTOR_NAND:
+ case kind::BITVECTOR_NOR:
+ {
+ bool allUnconstrained = true;
+ for (TNode child : parent)
+ {
+ if (d_unconstrained.find(child) == d_unconstrained.end())
+ {
+ allUnconstrained = false;
+ break;
+ }
+ }
+ if (allUnconstrained)
+ {
+ checkParent = true;
+ }
+ }
+ break;
+
+ // Require all children to be unconstrained and different
+ case kind::BITVECTOR_SHL:
+ case kind::BITVECTOR_LSHR:
+ case kind::BITVECTOR_ASHR:
+ case kind::BITVECTOR_UDIV_TOTAL:
+ case kind::BITVECTOR_UREM_TOTAL:
+ case kind::BITVECTOR_SDIV:
+ case kind::BITVECTOR_SREM:
+ case kind::BITVECTOR_SMOD:
+ {
+ bool allUnconstrained = true;
+ bool allDifferent = true;
+ for (TNode::iterator child_it = parent.begin();
+ child_it != parent.end();
+ ++child_it)
+ {
+ if (d_unconstrained.find(*child_it) == d_unconstrained.end())
+ {
+ allUnconstrained = false;
+ break;
+ }
+ for (TNode::iterator child_it2 = child_it + 1;
+ child_it2 != parent.end();
+ ++child_it2)
+ {
+ if (*child_it == *child_it2)
+ {
+ allDifferent = false;
+ break;
+ }
+ }
+ }
+ if (allUnconstrained && allDifferent)
+ {
+ checkParent = true;
+ }
+ break;
+ }
+
+ // Requires all children to be unconstrained and different, and returns
+ // a different type
+ case kind::BITVECTOR_CONCAT:
+ {
+ bool allUnconstrained = true;
+ bool allDifferent = true;
+ for (TNode::iterator child_it = parent.begin();
+ child_it != parent.end();
+ ++child_it)
+ {
+ if (d_unconstrained.find(*child_it) == d_unconstrained.end())
+ {
+ allUnconstrained = false;
+ break;
+ }
+ for (TNode::iterator child_it2 = child_it + 1;
+ child_it2 != parent.end();
+ ++child_it2)
+ {
+ if (*child_it == *child_it2)
+ {
+ allDifferent = false;
+ break;
+ }
+ }
+ }
+ if (allUnconstrained && allDifferent)
+ {
+ if (d_unconstrained.find(parent) == d_unconstrained.end()
+ && !d_substitutions.hasSubstitution(parent))
+ {
+ ++d_numUnconstrainedElim;
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ currentSub = newUnconstrainedVar(parent.getType(), currentSub);
+ current = parent;
+ }
+ else
+ {
+ currentSub = Node();
+ }
+ }
+ }
+ break;
+
+ // N-ary operators returning same type requiring at least one child to
+ // be unconstrained
+ case kind::PLUS:
+ case kind::MINUS:
+ if (current.getType().isInteger() && !parent.getType().isInteger())
+ {
+ break;
+ }
+ case kind::XOR:
+ case kind::BITVECTOR_XOR:
+ case kind::BITVECTOR_XNOR:
+ case kind::BITVECTOR_PLUS:
+ case kind::BITVECTOR_SUB: checkParent = true; break;
+
+ // Multiplication/division: must be non-integer and other operand must
+ // be non-zero
+ case kind::MULT:
+ case kind::DIVISION:
+ {
+ Assert(parent.getNumChildren() == 2);
+ TNode other;
+ if (parent[0] == current)
+ {
+ other = parent[1];
+ }
+ else
+ {
+ Assert(parent[1] == current);
+ other = parent[0];
+ }
+ if (d_unconstrained.find(other) != d_unconstrained.end())
+ {
+ if (d_unconstrained.find(parent) == d_unconstrained.end()
+ && !d_substitutions.hasSubstitution(parent))
+ {
+ if (current.getType().isInteger() && other.getType().isInteger())
+ {
+ Assert(parent.getKind() == kind::DIVISION
+ || parent.getType().isInteger());
+ if (parent.getKind() == kind::DIVISION)
+ {
+ break;
+ }
+ }
+ ++d_numUnconstrainedElim;
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ current = parent;
+ }
+ else
+ {
+ currentSub = Node();
+ }
+ }
+ else
+ {
+ // if only the denominator of a division is unconstrained, can't
+ // set it to 0 so the result is not unconstrained
+ if (parent.getKind() == kind::DIVISION && current == parent[1])
+ {
+ break;
+ }
+ // if we are an integer, the only way we are unconstrained is if
+ // we are a MULT by -1
+ if (current.getType().isInteger())
+ {
+ // div/mult by 1 should have been simplified
+ Assert(other != nm->mkConst<Rational>(1));
+ // div by -1 should have been simplified
+ if (other != nm->mkConst<Rational>(-1))
+ {
+ break;
+ }
+ else
+ {
+ Assert(parent.getKind() == kind::MULT);
+ Assert(parent.getType().isInteger());
+ }
+ }
+ else
+ {
+ // TODO(#2377): could build ITE here
+ Node test = other.eqNode(nm->mkConst<Rational>(0));
+ if (Rewriter::rewrite(test) != nm->mkConst<bool>(false))
+ {
+ break;
+ }
+ }
+ ++d_numUnconstrainedElim;
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ current = parent;
+ }
+ break;
+ }
+
+ // Bitvector MULT - current must only appear once in the children:
+ // all other children must be unconstrained or odd
+ case kind::BITVECTOR_MULT:
+ {
+ bool found = false;
+ bool done = false;
+
+ for (TNode child : parent)
+ {
+ if (child == current)
+ {
+ if (found)
+ {
+ done = true;
+ break;
+ }
+ found = true;
+ continue;
+ }
+ else if (d_unconstrained.find(child) == d_unconstrained.end())
+ {
+ Node extractOp =
+ nm->mkConst<BitVectorExtract>(BitVectorExtract(0, 0));
+ vector<Node> children;
+ children.push_back(child);
+ Node test = nm->mkNode(extractOp, children);
+ BitVector one(1, unsigned(1));
+ test = test.eqNode(nm->mkConst<BitVector>(one));
+ if (Rewriter::rewrite(test) != nm->mkConst<bool>(true))
+ {
+ done = true;
+ break;
+ }
+ }
+ }
+ if (done)
+ {
+ break;
+ }
+ checkParent = true;
+ break;
+ }
+
+ // Uninterpreted function - if domain is infinite, no quantifiers are
+ // used, and any child is unconstrained, result is unconstrained
+ case kind::APPLY_UF:
+ if (d_logicInfo.isQuantified()
+ || !current.getType().getCardinality().isInfinite())
+ {
+ break;
+ }
+ if (d_unconstrained.find(parent) == d_unconstrained.end()
+ && !d_substitutions.hasSubstitution(parent))
+ {
+ ++d_numUnconstrainedElim;
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ if (parent.getType() != current.getType())
+ {
+ currentSub = newUnconstrainedVar(parent.getType(), currentSub);
+ }
+ current = parent;
+ }
+ else
+ {
+ currentSub = Node();
+ }
+ break;
+
+ // Array select - if array is unconstrained, so is result
+ case kind::SELECT:
+ if (parent[0] == current)
+ {
+ ++d_numUnconstrainedElim;
+ Assert(current.getType().isArray());
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ currentSub = newUnconstrainedVar(
+ current.getType().getArrayConstituentType(), currentSub);
+ current = parent;
+ }
+ break;
+
+ // Array store - if both store and value are unconstrained, so is
+ // resulting store
+ case kind::STORE:
+ if (((parent[0] == current
+ && d_unconstrained.find(parent[2]) != d_unconstrained.end())
+ || (parent[2] == current
+ && d_unconstrained.find(parent[0])
+ != d_unconstrained.end())))
+ {
+ if (d_unconstrained.find(parent) == d_unconstrained.end()
+ && !d_substitutions.hasSubstitution(parent))
+ {
+ ++d_numUnconstrainedElim;
+ if (parent[0] != current)
+ {
+ if (parent[0].isVar())
+ {
+ currentSub = parent[0];
+ }
+ else
+ {
+ Assert(d_substitutions.hasSubstitution(parent[0]));
+ currentSub = d_substitutions.apply(parent[0]);
+ }
+ }
+ else if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ current = parent;
+ }
+ else
+ {
+ currentSub = Node();
+ }
+ }
+ break;
+
+ // Bit-vector comparisons: replace with new Boolean variable, but have
+ // to also conjoin with a side condition as there is always one case
+ // when the comparison is forced to be false
+ case kind::BITVECTOR_ULT:
+ case kind::BITVECTOR_UGE:
+ case kind::BITVECTOR_UGT:
+ case kind::BITVECTOR_ULE:
+ case kind::BITVECTOR_SLT:
+ case kind::BITVECTOR_SGE:
+ case kind::BITVECTOR_SGT:
+ case kind::BITVECTOR_SLE:
+ {
+ // Tuples over (signed, swap, strict).
+ switch (parent.getKind())
+ {
+ case kind::BITVECTOR_UGE: break;
+ case kind::BITVECTOR_ULT: strict = true; break;
+ case kind::BITVECTOR_ULE: swap = true; break;
+ case kind::BITVECTOR_UGT:
+ swap = true;
+ strict = true;
+ break;
+ case kind::BITVECTOR_SGE: isSigned = true; break;
+ case kind::BITVECTOR_SLT:
+ isSigned = true;
+ strict = true;
+ break;
+ case kind::BITVECTOR_SLE:
+ isSigned = true;
+ swap = true;
+ break;
+ case kind::BITVECTOR_SGT:
+ isSigned = true;
+ swap = true;
+ strict = true;
+ break;
+ default: Unreachable();
+ }
+ TNode other;
+ bool left = false;
+ if (parent[0] == current)
+ {
+ other = parent[1];
+ left = true;
+ }
+ else
+ {
+ Assert(parent[1] == current);
+ other = parent[0];
+ }
+ if (d_unconstrained.find(other) != d_unconstrained.end())
+ {
+ if (d_unconstrained.find(parent) == d_unconstrained.end()
+ && !d_substitutions.hasSubstitution(parent))
+ {
+ ++d_numUnconstrainedElim;
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ currentSub = newUnconstrainedVar(parent.getType(), currentSub);
+ current = parent;
+ }
+ else
+ {
+ currentSub = Node();
+ }
+ }
+ else
+ {
+ unsigned size = current.getType().getBitVectorSize();
+ BitVector bv =
+ isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1))
+ : BitVector(size, unsigned(0));
+ if (swap == left)
+ {
+ bv = ~bv;
+ }
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ currentSub = newUnconstrainedVar(parent.getType(), currentSub);
+ current = parent;
+ Node test =
+ Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
+ if (test == nm->mkConst<bool>(false))
+ {
+ break;
+ }
+ currentSub = strict ? currentSub.andNode(test.notNode())
+ : currentSub.orNode(test);
+ // Delay adding this substitution - see comment at end of function
+ delayQueueLeft.push_back(current);
+ delayQueueRight.push_back(currentSub);
+ currentSub = Node();
+ parent = TNode();
+ }
+ break;
+ }
+
+ // Do nothing
+ case kind::BITVECTOR_SIGN_EXTEND:
+ case kind::BITVECTOR_ZERO_EXTEND:
+ case kind::BITVECTOR_REPEAT:
+ case kind::BITVECTOR_ROTATE_LEFT:
+ case kind::BITVECTOR_ROTATE_RIGHT:
+
+ default: break;
+ }
+ if (checkParent)
+ {
+ // run for various cases from above
+ if (d_unconstrained.find(parent) == d_unconstrained.end()
+ && !d_substitutions.hasSubstitution(parent))
+ {
+ ++d_numUnconstrainedElim;
+ if (currentSub.isNull())
+ {
+ currentSub = current;
+ }
+ current = parent;
+ }
+ else
+ {
+ currentSub = Node();
+ }
+ }
+ if (current == parent && d_visited[parent] == 1)
+ {
+ d_unconstrained.insert(parent);
+ continue;
+ }
+ }
+ if (!currentSub.isNull())
+ {
+ Assert(currentSub.isVar());
+ d_substitutions.addSubstitution(current, currentSub, false);
+ }
+ if (workList.empty())
+ {
+ break;
+ }
+ current = workList.back();
+ currentSub = Node();
+ workList.pop_back();
+ }
+ TNode left;
+ Node right;
+ // All substitutions except those arising from bitvector comparisons are
+ // substitutions t -> x where x is a variable. This allows us to build the
+ // substitution very quickly (never invalidating the substitution cache).
+ // Bitvector comparisons are more complicated and may require
+ // back-substitution and cache-invalidation. So we do these last.
+ while (!delayQueueLeft.empty())
+ {
+ left = delayQueueLeft.back();
+ if (!d_substitutions.hasSubstitution(left))
+ {
+ right = d_substitutions.apply(delayQueueRight.back());
+ d_substitutions.addSubstitution(delayQueueLeft.back(), right);
+ }
+ delayQueueLeft.pop_back();
+ delayQueueRight.pop_back();
+ }
+}
+
+PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ d_preprocContext->spendResource(options::preprocessStep());
+
+ std::vector<Node>& assertions = assertionsToPreprocess->ref();
+
+ d_context->push();
+
+ for (const Node& assertion : assertions)
+ {
+ visitAll(assertion);
+ }
+
+ if (!d_unconstrained.empty())
+ {
+ processUnconstrained();
+ // d_substitutions.print(Message.getStream());
+ for (Node& assertion : assertions)
+ {
+ assertion = Rewriter::rewrite(d_substitutions.apply(assertion));
+ }
+ }
+
+ // to clear substitutions map
+ d_context->pop();
+
+ d_visited.clear();
+ d_visitedOnce.clear();
+ d_unconstrained.clear();
+
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
new file mode 100644
index 000000000..658834ee3
--- /dev/null
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -0,0 +1,75 @@
+/********************* */
+/*! \file unconstrained_simplifier.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Clark Barrett, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Simplifications based on unconstrained variables
+ **
+ ** This module implements a preprocessing phase which replaces certain
+ ** "unconstrained" expressions by variables. Based on Roberto
+ ** Bruttomesso's PhD thesis.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
+#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
+
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/logic_info.h"
+#include "theory/substitutions.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class UnconstrainedSimplifier : public PreprocessingPass
+{
+ public:
+ UnconstrainedSimplifier(PreprocessingPassContext* preprocContext);
+ ~UnconstrainedSimplifier() override;
+
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ /** number of expressions eliminated due to unconstrained simplification */
+ IntStat d_numUnconstrainedElim;
+
+ using TNodeCountMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>;
+ using TNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>;
+ using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
+
+ TNodeCountMap d_visited;
+ TNodeMap d_visitedOnce;
+ TNodeSet d_unconstrained;
+
+ context::Context* d_context;
+ theory::SubstitutionMap d_substitutions;
+
+ const LogicInfo& d_logicInfo;
+
+ void visitAll(TNode assertion);
+ Node newUnconstrainedVar(TypeNode t, TNode var);
+ void processUnconstrained();
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 97fa32d17..4143f2d4b 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -39,6 +39,7 @@
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/smt_engine_scope.h"
#include "smt/term_formula_removal.h"
+#include "theory/logic_info.h"
#include "theory/substitutions.h"
namespace CVC4 {
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index a289752fa..96e554680 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -43,6 +43,7 @@ class PreprocessingPassContext
DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
context::Context* getUserContext() { return d_smt->d_userContext; }
+ context::Context* getDecisionContext() { return d_smt->d_context; }
RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
void spendResource(unsigned amount)
@@ -50,6 +51,8 @@ class PreprocessingPassContext
d_resourceManager->spendResource(amount);
}
+ const LogicInfo& getLogicInfo() { return d_smt->d_logic; }
+
/* Widen the logic to include the given theory. */
void widenLogic(theory::TheoryId id);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback