prop/cryptominisat.cpp \
prop/theory_proxy.cpp \
prop/theory_proxy.h \
- smt/boolean_terms.cpp \
- smt/boolean_terms.h \
smt/command.cpp \
smt/command.h \
smt/command_list.cpp \
smt/command_list.h \
smt/dump.cpp \
smt/dump.h \
- smt/ite_removal.cpp \
- smt/ite_removal.h \
+ smt/term_formula_removal.cpp \
+ smt/term_formula_removal.h \
smt/logic_exception.h \
smt/logic_request.cpp \
smt/logic_request.h \
smt/managed_ostreams.h \
smt/model.cpp \
smt/model.h \
- smt/model_postprocessor.cpp \
- smt/model_postprocessor.h \
smt/smt_engine.cpp \
smt/smt_engine.h \
smt/smt_engine_check_proof.cpp \
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "prop/sat_solver_types.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
#include "smt/smt_engine_scope.h"
using namespace std;
#define __CVC4__DECISION__DECISION_STRATEGY_H
#include "prop/sat_solver_types.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
namespace CVC4 {
#include "expr/node_manager.h"
#include "options/decision_options.h"
#include "theory/rewriter.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
#include "smt/smt_statistics_registry.h"
namespace CVC4 {
argument_extender_implementation.h \
argument_extender.h \
base_handlers.h \
- boolean_term_conversion_mode.cpp \
- boolean_term_conversion_mode.h \
bv_bitblast_mode.cpp \
bv_bitblast_mode.h \
decision_mode.cpp \
+++ /dev/null
-/********************* */
-/*! \file boolean_term_conversion_mode.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-#include "options/boolean_term_conversion_mode.h"
-
-#include <iostream>
-
-namespace CVC4 {
-
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file boolean_term_conversion_mode.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
-#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
-
-#include <iosfwd>
-
-namespace CVC4 {
-namespace theory {
-namespace booleans {
-
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */
#include "options/arith_propagation_mode.h"
#include "options/arith_unate_lemma_mode.h"
#include "options/base_options.h"
-#include "options/boolean_term_conversion_mode.h"
#include "options/bv_bitblast_mode.h"
#include "options/bv_options.h"
#include "options/decision_mode.h"
#include "options/arith_propagation_mode.h"
#include "options/arith_unate_lemma_mode.h"
#include "options/base_handlers.h"
-#include "options/boolean_term_conversion_mode.h"
#include "options/bv_bitblast_mode.h"
#include "options/decision_mode.h"
#include "options/language.h"
+++ /dev/null
-/********************* */
-/*! \file boolean_terms.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-#include "smt/boolean_terms.h"
-
-#include <algorithm>
-#include <map>
-#include <set>
-#include <stack>
-#include <string>
-
-#include "expr/kind.h"
-#include "expr/node_manager_attributes.h"
-#include "options/boolean_term_conversion_mode.h"
-#include "options/booleans_options.h"
-#include "smt/smt_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/theory_model.h"
-#include "util/ntuple.h"
-
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::booleans;
-
-namespace CVC4 {
-namespace smt {
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file boolean_terms.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include "expr/attribute.h"
-#include "expr/node.h"
-#include "util/hash.h"
-#include <map>
-#include <utility>
-
-namespace CVC4 {
-namespace smt {
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file ite_removal.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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 Removal of term ITEs
- **
- ** Removal of term ITEs.
- **/
-#include "smt/ite_removal.h"
-
-#include <vector>
-
-#include "options/proof_options.h"
-#include "proof/proof_manager.h"
-#include "theory/ite_utilities.h"
-
-using namespace std;
-
-namespace CVC4 {
-
-RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
- : d_iteCache(u)
-{
- d_containsVisitor = new theory::ContainsTermITEVisitor();
-}
-
-RemoveTermFormulas::~RemoveTermFormulas(){
- delete d_containsVisitor;
-}
-
-void RemoveTermFormulas::garbageCollect(){
- d_containsVisitor->garbageCollect();
-}
-
-theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() {
- return d_containsVisitor;
-}
-
-size_t RemoveTermFormulas::collectedCacheSizes() const{
- return d_containsVisitor->cache_size() + d_iteCache.size();
-}
-
-void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
-{
- size_t n = output.size();
- for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
- // Do this in two steps to avoid Node problems(?)
- // Appears related to bug 512, splitting this into two lines
- // fixes the bug on clang on Mac OS
- Node itesRemoved = run(output[i], output, iteSkolemMap, false, false);
- // In some calling contexts, not necessary to report dependence information.
- if (reportDeps &&
- (options::unsatCores() || options::fewerPreprocessingHoles())) {
- // new assertions have a dependence on the node
- PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
- while(n < output.size()) {
- PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
- ++n;
- }
- }
- output[i] = itesRemoved;
- }
-}
-
-bool RemoveTermFormulas::containsTermITE(TNode e) const {
- return d_containsVisitor->containsTermITE(e);
-}
-
-Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) {
- // Current node
- Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl;
-
- //if(node.isVar() || node.isConst()){
- // (options::biasedITERemoval() && !containsTermITE(node))){
- //if(node.isVar()){
- // return Node(node);
- //}
- if( node.getKind()==kind::INST_PATTERN_LIST ){
- return Node(node);
- }
-
- // The result may be cached already
- int cv = cacheVal( inQuant, inTerm );
- std::pair<Node, int> cacheKey(node, cv);
- NodeManager *nodeManager = NodeManager::currentNM();
- ITECache::const_iterator i = d_iteCache.find(cacheKey);
- if(i != d_iteCache.end()) {
- Node cached = (*i).second;
- Debug("ite") << "removeITEs: in-cache: " << cached << endl;
- return cached.isNull() ? Node(node) : cached;
- }
-
-
- // If an ITE, replace it
- TypeNode nodeType = node.getType();
- if(node.getKind() == kind::ITE) {
- if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
- Node skolem;
- // Make the skolem to represent the ITE
- skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
-
- // The new assertion
- Node newAssertion =
- nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
- skolem.eqNode(node[2]));
- Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
-
- // Attach the skolem
- d_iteCache.insert(cacheKey, skolem);
-
- // Remove ITEs from the new assertion, rewrite it and push it to the output
- newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
-
- iteSkolemMap[skolem] = output.size();
- output.push_back(newAssertion);
-
- // The representation is now the skolem
- return skolem;
- }
- }
- //if a non-variable Boolean term, replace it
- if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){
- Node skolem;
- // Make the skolem to represent the Boolean term
- //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal");
- skolem = nodeManager->mkBooleanTermVariable();
-
- // The new assertion
- Node newAssertion = skolem.eqNode( node );
- Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
-
- // Attach the skolem
- d_iteCache.insert(cacheKey, skolem);
-
- // Remove ITEs from the new assertion, rewrite it and push it to the output
- newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
-
- iteSkolemMap[skolem] = output.size();
- output.push_back(newAssertion);
-
- // The representation is now the skolem
- return skolem;
- }
-
- if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
- // Remember if we're inside a quantifier
- inQuant = true;
- }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL &&
- node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR &&
- node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){
- // Remember if we're inside a term
- Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl;
- inTerm = true;
- }
-
- // If not an ITE, go deep
- vector<Node> newChildren;
- bool somethingChanged = false;
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- newChildren.push_back(node.getOperator());
- }
- // Remove the ITEs from the children
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm);
- somethingChanged |= (newChild != *it);
- newChildren.push_back(newChild);
- }
-
- // If changes, we rewrite
- if(somethingChanged) {
- Node cached = nodeManager->mkNode(node.getKind(), newChildren);
- d_iteCache.insert(cacheKey, cached);
- return cached;
- } else {
- d_iteCache.insert(cacheKey, Node::null());
- return node;
- }
-}
-
-Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
- //if(node.isVar() || node.isConst()){
- // (options::biasedITERemoval() && !containsTermITE(node))){
- //if(node.isVar()){
- // return Node(node);
- //}
- if( node.getKind()==kind::INST_PATTERN_LIST ){
- return Node(node);
- }
-
- // Check the cache
- NodeManager *nodeManager = NodeManager::currentNM();
- int cv = cacheVal( inQuant, inTerm );
- ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv));
- if(i != d_iteCache.end()) {
- Node cached = (*i).second;
- return cached.isNull() ? Node(node) : cached;
- }
-
- if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
- // Remember if we're inside a quantifier
- inQuant = true;
- }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){
- // Remember if we're inside a term
- inTerm = true;
- }
-
- vector<Node> newChildren;
- bool somethingChanged = false;
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- newChildren.push_back(node.getOperator());
- }
- // Replace in children
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = replace(*it, inQuant, inTerm);
- somethingChanged |= (newChild != *it);
- newChildren.push_back(newChild);
- }
-
- // If changes, we rewrite
- if(somethingChanged) {
- return nodeManager->mkNode(node.getKind(), newChildren);
- } else {
- return node;
- }
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file ite_removal.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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 Removal of term ITEs
- **
- ** Removal of term ITEs.
- **/
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include <vector>
-
-#include "context/cdinsert_hashmap.h"
-#include "context/context.h"
-#include "expr/node.h"
-#include "smt/dump.h"
-#include "util/bool.h"
-#include "util/hash.h"
-
-namespace CVC4 {
-
-namespace theory {
- class ContainsTermITEVisitor;
-}/* CVC4::theory namespace */
-
-typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
-
-class RemoveTermFormulas {
- typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache;
- ITECache d_iteCache;
-
- static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); }
-public:
-
- RemoveTermFormulas(context::UserContext* u);
- ~RemoveTermFormulas();
-
- /**
- * Removes the ITE nodes by introducing skolem variables. All
- * additional assertions are pushed into assertions. iteSkolemMap
- * contains a map from introduced skolem variables to the index in
- * assertions containing the new Boolean ite created in conjunction
- * with that skolem variable.
- *
- * With reportDeps true, report reasoning dependences to the proof
- * manager (for unsat cores).
- */
- void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
-
- /**
- * Removes the ITE from the node by introducing skolem
- * variables. All additional assertions are pushed into
- * assertions. iteSkolemMap contains a map from introduced skolem
- * variables to the index in assertions containing the new Boolean
- * ite created in conjunction with that skolem variable.
- */
- Node run(TNode node, std::vector<Node>& additionalAssertions,
- IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm);
-
- /**
- * Substitute under node using pre-existing cache. Do not remove
- * any ITEs not seen during previous runs.
- */
- Node replace(TNode node, bool inQuant = false, bool inTerm = false) const;
-
- /** Returns true if e contains a term ite. */
- bool containsTermITE(TNode e) const;
-
- /** Returns the collected size of the caches. */
- size_t collectedCacheSizes() const;
-
- /** Garbage collects non-context dependent data-structures. */
- void garbageCollect();
-
- /** Return the RemoveTermFormulas's containsVisitor. */
- theory::ContainsTermITEVisitor* getContainsVisitor();
-
-private:
- theory::ContainsTermITEVisitor* d_containsVisitor;
-
-};/* class RemoveTTE */
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file model_postprocessor.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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
- **
- **
- **/
-
-#include "smt/model_postprocessor.h"
-
-#include "expr/node_manager_attributes.h"
-#include "expr/record.h"
-#include "smt/boolean_terms.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace smt {
-
-
-} /* namespace smt */
-} /* namespace CVC4 */
+++ /dev/null
-/********************* */
-/*! \file model_postprocessor.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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
- **
- **
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__MODEL_POSTPROCESSOR_H
-#define __CVC4__MODEL_POSTPROCESSOR_H
-
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace smt {
-
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__MODEL_POSTPROCESSOR_H */
#include "options/arith_options.h"
#include "options/arrays_options.h"
#include "options/base_options.h"
-#include "options/boolean_term_conversion_mode.h"
-#include "options/booleans_options.h"
#include "options/booleans_options.h"
#include "options/bv_options.h"
#include "options/datatypes_options.h"
#include "proof/theory_proof.h"
#include "proof/unsat_core.h"
#include "prop/prop_engine.h"
-#include "smt/boolean_terms.h"
#include "smt/command.h"
#include "smt/command_list.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
#include "smt/logic_request.h"
#include "smt/managed_ostreams.h"
-#include "smt/model_postprocessor.h"
#include "smt/smt_engine_scope.h"
#include "smt/update_ostream.h"
#include "smt_util/boolean_simplification.h"
}/* SmtEngine::assertFormula() */
Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
-/*
- ModelPostprocessor mpost;
- NodeVisitor<ModelPostprocessor> visitor;
- Node value = visitor.run(mpost, node);
- Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
- Node realValue = mpost.rewriteAs(value, expectedType);
- Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl;
- if(options::condenseFunctionValues()) {
- realValue = Rewriter::rewrite(realValue);
- Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl;
- }
- return realValue;
- */
return node;
}
--- /dev/null
+/********************* */
+/*! \file term_formula_removal.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 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 Removal of term formulas
+ **
+ ** Removal of term formulas.
+ **/
+#include "smt/term_formula_removal.h"
+
+#include <vector>
+
+#include "options/proof_options.h"
+#include "proof/proof_manager.h"
+#include "theory/ite_utilities.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
+ : d_iteCache(u)
+{
+ d_containsVisitor = new theory::ContainsTermITEVisitor();
+}
+
+RemoveTermFormulas::~RemoveTermFormulas(){
+ delete d_containsVisitor;
+}
+
+void RemoveTermFormulas::garbageCollect(){
+ d_containsVisitor->garbageCollect();
+}
+
+theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() {
+ return d_containsVisitor;
+}
+
+size_t RemoveTermFormulas::collectedCacheSizes() const{
+ return d_containsVisitor->cache_size() + d_iteCache.size();
+}
+
+void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
+{
+ size_t n = output.size();
+ for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
+ // Do this in two steps to avoid Node problems(?)
+ // Appears related to bug 512, splitting this into two lines
+ // fixes the bug on clang on Mac OS
+ Node itesRemoved = run(output[i], output, iteSkolemMap, false, false);
+ // In some calling contexts, not necessary to report dependence information.
+ if (reportDeps &&
+ (options::unsatCores() || options::fewerPreprocessingHoles())) {
+ // new assertions have a dependence on the node
+ PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
+ while(n < output.size()) {
+ PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
+ ++n;
+ }
+ }
+ output[i] = itesRemoved;
+ }
+}
+
+bool RemoveTermFormulas::containsTermITE(TNode e) const {
+ return d_containsVisitor->containsTermITE(e);
+}
+
+Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
+ IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) {
+ // Current node
+ Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl;
+
+ //if(node.isVar() || node.isConst()){
+ // (options::biasedITERemoval() && !containsTermITE(node))){
+ //if(node.isVar()){
+ // return Node(node);
+ //}
+ if( node.getKind()==kind::INST_PATTERN_LIST ){
+ return Node(node);
+ }
+
+ // The result may be cached already
+ int cv = cacheVal( inQuant, inTerm );
+ std::pair<Node, int> cacheKey(node, cv);
+ NodeManager *nodeManager = NodeManager::currentNM();
+ ITECache::const_iterator i = d_iteCache.find(cacheKey);
+ if(i != d_iteCache.end()) {
+ Node cached = (*i).second;
+ Debug("ite") << "removeITEs: in-cache: " << cached << endl;
+ return cached.isNull() ? Node(node) : cached;
+ }
+
+
+ // If an ITE, replace it
+ TypeNode nodeType = node.getType();
+ if(node.getKind() == kind::ITE) {
+ if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
+ Node skolem;
+ // Make the skolem to represent the ITE
+ skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
+
+ // The new assertion
+ Node newAssertion =
+ nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
+ skolem.eqNode(node[2]));
+ Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
+
+ // Attach the skolem
+ d_iteCache.insert(cacheKey, skolem);
+
+ // Remove ITEs from the new assertion, rewrite it and push it to the output
+ newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
+
+ iteSkolemMap[skolem] = output.size();
+ output.push_back(newAssertion);
+
+ // The representation is now the skolem
+ return skolem;
+ }
+ }
+ //if a non-variable Boolean term, replace it
+ if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){
+ Node skolem;
+ // Make the skolem to represent the Boolean term
+ //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal");
+ skolem = nodeManager->mkBooleanTermVariable();
+
+ // The new assertion
+ Node newAssertion = skolem.eqNode( node );
+ Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
+
+ // Attach the skolem
+ d_iteCache.insert(cacheKey, skolem);
+
+ // Remove ITEs from the new assertion, rewrite it and push it to the output
+ newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
+
+ iteSkolemMap[skolem] = output.size();
+ output.push_back(newAssertion);
+
+ // The representation is now the skolem
+ return skolem;
+ }
+
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ // Remember if we're inside a quantifier
+ inQuant = true;
+ }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL &&
+ node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR &&
+ node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){
+ // Remember if we're inside a term
+ Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl;
+ inTerm = true;
+ }
+
+ // If not an ITE, go deep
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Remove the ITEs from the children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ // If changes, we rewrite
+ if(somethingChanged) {
+ Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+ d_iteCache.insert(cacheKey, cached);
+ return cached;
+ } else {
+ d_iteCache.insert(cacheKey, Node::null());
+ return node;
+ }
+}
+
+Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
+ //if(node.isVar() || node.isConst()){
+ // (options::biasedITERemoval() && !containsTermITE(node))){
+ //if(node.isVar()){
+ // return Node(node);
+ //}
+ if( node.getKind()==kind::INST_PATTERN_LIST ){
+ return Node(node);
+ }
+
+ // Check the cache
+ NodeManager *nodeManager = NodeManager::currentNM();
+ int cv = cacheVal( inQuant, inTerm );
+ ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv));
+ if(i != d_iteCache.end()) {
+ Node cached = (*i).second;
+ return cached.isNull() ? Node(node) : cached;
+ }
+
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ // Remember if we're inside a quantifier
+ inQuant = true;
+ }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){
+ // Remember if we're inside a term
+ inTerm = true;
+ }
+
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Replace in children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = replace(*it, inQuant, inTerm);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ // If changes, we rewrite
+ if(somethingChanged) {
+ return nodeManager->mkNode(node.getKind(), newChildren);
+ } else {
+ return node;
+ }
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file term_formula_removal.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 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 Removal of term formulas
+ **
+ ** Removal of term formulas.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+
+#include "context/cdinsert_hashmap.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "smt/dump.h"
+#include "util/bool.h"
+#include "util/hash.h"
+
+namespace CVC4 {
+
+namespace theory {
+ class ContainsTermITEVisitor;
+}/* CVC4::theory namespace */
+
+typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
+
+class RemoveTermFormulas {
+ typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache;
+ ITECache d_iteCache;
+
+ static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); }
+public:
+
+ RemoveTermFormulas(context::UserContext* u);
+ ~RemoveTermFormulas();
+
+ /**
+ * Removes the ITE nodes by introducing skolem variables. All
+ * additional assertions are pushed into assertions. iteSkolemMap
+ * contains a map from introduced skolem variables to the index in
+ * assertions containing the new Boolean ite created in conjunction
+ * with that skolem variable.
+ *
+ * With reportDeps true, report reasoning dependences to the proof
+ * manager (for unsat cores).
+ */
+ void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
+
+ /**
+ * Removes the ITE from the node by introducing skolem
+ * variables. All additional assertions are pushed into
+ * assertions. iteSkolemMap contains a map from introduced skolem
+ * variables to the index in assertions containing the new Boolean
+ * ite created in conjunction with that skolem variable.
+ */
+ Node run(TNode node, std::vector<Node>& additionalAssertions,
+ IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm);
+
+ /**
+ * Substitute under node using pre-existing cache. Do not remove
+ * any ITEs not seen during previous runs.
+ */
+ Node replace(TNode node, bool inQuant = false, bool inTerm = false) const;
+
+ /** Returns true if e contains a term ite. */
+ bool containsTermITE(TNode e) const;
+
+ /** Returns the collected size of the caches. */
+ size_t collectedCacheSizes() const;
+
+ /** Garbage collects non-context dependent data-structures. */
+ void garbageCollect();
+
+ /** Return the RemoveTermFormulas's containsVisitor. */
+ theory::ContainsTermITEVisitor* getContainsVisitor();
+
+private:
+ theory::ContainsTermITEVisitor* d_containsVisitor;
+
+};/* class RemoveTTE */
+
+}/* CVC4 namespace */
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
-#include "smt/boolean_terms.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/theory_datatypes_type_rules.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/ceg_t_instantiator.h"
#include "options/quantifiers_options.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/inst_strategy_cbqi.h"
#include "options/quantifiers_options.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/theory_arith_private.h"
#include "proof/lemma_proof.h"
#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
#include "smt/logic_exception.h"
#include "smt_util/lemma_output_channel.h"
#include "smt_util/node_visitor.h"
projects / cvc5.git / commitdiff