summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am4
-rw-r--r--src/theory/quantifiers/ematching/candidate_generator.cpp (renamed from src/theory/quantifiers/candidate_generator.cpp)2
-rw-r--r--src/theory/quantifiers/ematching/candidate_generator.h (renamed from src/theory/quantifiers/candidate_generator.h)0
-rw-r--r--src/theory/quantifiers/ematching/inst_match_generator.cpp44
-rw-r--r--src/theory/quantifiers/ematching/inst_match_generator.h26
-rw-r--r--src/theory/quantifiers/ematching/trigger.cpp23
-rw-r--r--src/theory/quantifiers/ematching/trigger.h2
7 files changed, 8 insertions, 93 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index c6f8a7ad1..6395a70bc 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -366,8 +366,6 @@ libcvc4_la_SOURCES = \
theory/quantifiers/anti_skolem.h \
theory/quantifiers/bv_inverter.cpp \
theory/quantifiers/bv_inverter.h \
- theory/quantifiers/candidate_generator.cpp \
- theory/quantifiers/candidate_generator.h \
theory/quantifiers/cegqi/ceg_instantiator.cpp \
theory/quantifiers/cegqi/ceg_instantiator.h \
theory/quantifiers/cegqi/ceg_t_instantiator.cpp \
@@ -378,6 +376,8 @@ libcvc4_la_SOURCES = \
theory/quantifiers/conjecture_generator.h \
theory/quantifiers/dynamic_rewrite.cpp \
theory/quantifiers/dynamic_rewrite.h \
+ theory/quantifiers/ematching/candidate_generator.cpp \
+ theory/quantifiers/ematching/candidate_generator.h \
theory/quantifiers/ematching/ho_trigger.cpp \
theory/quantifiers/ematching/ho_trigger.h \
theory/quantifiers/ematching/inst_match_generator.cpp \
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 699a93286..ea5e8592d 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -12,7 +12,7 @@
** \brief Implementation of theory uf candidate generator class
**/
-#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/ematching/candidate_generator.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/instantiate.h"
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index 4662d7c4c..4662d7c4c 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index c36597e3e..ec0a4039a 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -17,11 +17,11 @@
#include "expr/datatype.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/ematching/candidate_generator.h"
+#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers_engine.h"
using namespace std;
@@ -541,14 +541,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
}
Trace("var-trigger-debug") << "Is " << n << " a variable trigger?"
<< std::endl;
- if (Trigger::isBooleanTermTrigger(n))
- {
- VarMatchGeneratorBooleanTerm* vmg =
- new VarMatchGeneratorBooleanTerm(n[0], n[1]);
- Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0]
- << std::endl;
- return vmg;
- }
Node x;
if (options::purifyTriggers())
{
@@ -565,38 +557,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
return new InstMatchGenerator(n);
}
-VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) :
- InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) {
- d_children_types.push_back(var.getAttribute(InstVarNumAttribute()));
-}
-
-int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent)
-{
- int ret_val = -1;
- if( !d_eq_class.isNull() ){
- Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
- d_eq_class = Node::null();
- d_rm_prev = m.get(d_children_types[0]).isNull();
- if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
- {
- return -1;
- }else{
- ret_val = continueNextMatch(q, m, qe, tparent);
- if( ret_val>0 ){
- return ret_val;
- }
- }
- }
- if( d_rm_prev ){
- m.d_vals[d_children_types[0]] = Node::null();
- d_rm_prev = false;
- }
- return ret_val;
-}
-
VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute()));
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 6c38db13b..cbd5702a0 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -418,32 +418,6 @@ class InstMatchGenerator : public IMGenerator {
static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
};/* class InstMatchGenerator */
-/** match generator for Boolean term ITEs
-* This handles the special case of triggers that look like ite( x, BV1, BV0 ).
-*/
-class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
-public:
- VarMatchGeneratorBooleanTerm( Node var, Node comp );
-
- /** Reset */
- bool reset(Node eqc, QuantifiersEngine* qe) override
- {
- d_eq_class = eqc;
- return true;
- }
- /** Get the next match. */
- int getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
-
- private:
- /** stores the true branch of the Boolean ITE */
- Node d_comp;
- /** stores whether we have written a value for var in the current match. */
- bool d_rm_prev;
-};
-
/** match generator for purified terms
* This handles the special case of invertible terms like x+1 (see
* Trigger::getTermInversionVariable).
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 430d261a1..4039c632f 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -15,7 +15,7 @@
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/ematching/candidate_generator.h"
#include "theory/quantifiers/ematching/ho_trigger.h"
#include "theory/quantifiers/ematching/inst_match_generator.h"
#include "theory/quantifiers/instantiate.h"
@@ -262,9 +262,8 @@ bool Trigger::isUsable( Node n, Node q ){
return true;
}else{
std::map< Node, Node > coeffs;
- if( isBooleanTermTrigger( n ) ){
- return true;
- }else if( options::purifyTriggers() ){
+ if (options::purifyTriggers())
+ {
Node x = getInversionVariable( n );
if( !x.isNull() ){
return true;
@@ -522,22 +521,6 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
}
}
-bool Trigger::isBooleanTermTrigger( Node n ) {
- if( n.getKind()==ITE ){
- //check for boolean term converted to ITE
- if( n[0].getKind()==INST_CONSTANT &&
- n[1].getKind()==CONST_BITVECTOR &&
- n[2].getKind()==CONST_BITVECTOR ){
- if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
- n[1].getConst<BitVector>().toInteger()==1 &&
- n[2].getConst<BitVector>().toInteger()==0 ){
- return true;
- }
- }
- }
- return false;
-}
-
bool Trigger::isPureTheoryTrigger( Node n ) {
if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
return false;
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index cd10e4f8a..28d227bf7 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -315,8 +315,6 @@ class Trigger {
static bool isRelationalTriggerKind( Kind k );
/** is n a simple trigger (see inst_match_generator.h)? */
static bool isSimpleTrigger( Node n );
- /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */
- static bool isBooleanTermTrigger( Node n );
/** is n a pure theory trigger, e.g. head( x )? */
static bool isPureTheoryTrigger( Node n );
/** get trigger weight
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback