14 int ExprTransform::CountSubTerms(
const Expr& e,
int& counter) {
17 for (
int i = 0; i < e.
arity(); i++) {
18 int count = CountSubTerms(e[i], counter) + 1;
25 std::string ExprTransform::NewBryantVar(
const int a,
const int b){
27 std::stringstream out1, out2;
30 std::string Tempvar =
"A";
31 S = Tempvar + out1.str() +
"B" + out2.str();
39 for (T_generator_map::iterator f = generator_map.begin(); f != generator_map.end(); f++){
41 Type TempType = type_map.find((*f).first)->second;
43 for (set< Expr >::iterator p = (*f).second->begin(); p != (*f).second->end(); p++){
45 pair< Expr, Expr > key = pair< Expr, Expr >((*f).first, (*p));
46 std::string NewName = NewBryantVar(VarTotal, ArgVar);
47 Expr value = d_core->newVar(NewName, TempType);
48 name_map.insert( *
new pair< pair< Expr, Expr>,
Expr >(key, value));
55 void ExprTransform::PredConstrainer(set<Expr>& Not_replaced_set,
const Expr& e,
const Expr& Pred,
int location,
B_name_map& name_map, set<Expr>& SeenBefore, set<Expr>& Constrained_set,
T_generator_map& Constrained_map, set<Expr>& P_constrained_set) {
56 if (!SeenBefore.insert(e).second)
62 if (e[location].isVar() || Not_replaced_set.find(e[location]) != Not_replaced_set.end())
64 else Temp0 = name_map.find(pair<Expr, Expr>((e[location]).getOpExpr(),(e[location])))->second;
65 if (Pred[location].isVar())
66 Temp1 = Pred[location];
67 else Temp1 = name_map.find(pair<Expr, Expr>((Pred[location]).getOpExpr(),(Pred[location])))->second;
68 if (Constrained_set.find(e[location]) != Constrained_set.end()) {
73 if (P_constrained_set.find(Reflexor) == P_constrained_set.end())
74 P_constrained_set.insert(Eq);
80 if (Constrained_map.find(Pred[location]) == Constrained_map.end())
81 Constrained_map.insert(pair<
Expr, set<Expr>*>(Pred[location],
new set<Expr>));
82 Constrained_map[Pred[location]]->insert(Temp0);
90 for (
int l = 0; l < e.
arity(); l++)
91 PredConstrainer(Not_replaced_set, e[l], Pred, location, name_map, SeenBefore, Constrained_set, Constrained_map, P_constrained_set);
94 void ExprTransform::PredConstrainTester(set<Expr>& Not_replaced_set,
const Expr& e,
B_name_map& name_map, vector<Expr>& Pred_vec, set<Expr>& Constrained_set, set<Expr>& P_constrained_set,
T_generator_map& Constrained_map) {
95 for (vector<Expr>::iterator i = Pred_vec.begin(); i != Pred_vec.end(); i++) {
96 for (
int k = 0; k < (*i).arity(); k++)
97 if (Constrained_set.find((*i)[k]) != Constrained_set.end()){
99 PredConstrainer(Not_replaced_set, e, (*i), k, name_map, SeenBefore, Constrained_set, Constrained_map, P_constrained_set);
114 for (vector<Expr>::reverse_iterator f = (Creation_map.find(Orig.
getOpExpr())->second->rbegin());
115 f != (Creation_map.find(Orig.
getOpExpr())->second->rend()); f++) {
116 if ((*f).getOpExpr() == Orig.
getOpExpr()) {
118 for (
int i = 0; i < Orig.
arity(); i++) {
120 if ((*f)[i].isApply())
121 TempEqExpr = ITE_map.find((*f)[i])->second;
123 TempEqExpr = (*f)[i];
124 if (Orig[i].isApply())
125 TempEqExpr = TempEqExpr.
eqExpr(ITE_map.find(Orig[i])->second);
127 TempEqExpr = TempEqExpr.
eqExpr(Orig[i]);
128 if (TempExpr.
isNull() ==
true)
129 TempExpr = TempEqExpr;
131 TempExpr = TempExpr.
andExpr(TempEqExpr);
133 if (NewITE.
isNull() ==
true)
134 NewITE = TempExpr.
iteExpr(name_map.find(pair<Expr, Expr>((*f).getOpExpr(),(*f)))->second, Value);
137 NewITE = TempExpr.
iteExpr(name_map.find(pair<Expr, Expr>((*f).getOpExpr(),(*f)))->second, Temp);
152 for (T_ITE_vec::iterator f = ITE_vec.begin(); f != ITE_vec.end(); f++) {
154 if (Creation_map.find((*f).getOpExpr()) == Creation_map.end()) {
155 Creation_map.insert(pair<
Expr, vector<Expr>*> (
156 (*f).getOpExpr(),
new vector<Expr> ()));
157 Creation_map[(*f).getOpExpr()]->push_back((*f));
158 if (instance_map[(*f).getOpExpr()] <
LIMIT || !(*f).isTerm())
159 ITE_map.insert(pair<Expr, Expr> ((*f), name_map.find(pair<
160 Expr,
Expr> ((*f).getOpExpr(), (*f)))->second));
162 ITE_map.insert(pair<Expr, Expr> ((*f), (*f)));
163 Not_replaced_set.insert(*f);
166 if (instance_map[(*f).getOpExpr()] >
LIMIT && (*f).isTerm()) {
167 ITE_map.insert(pair<Expr, Expr> ((*f), (*f)));
168 Creation_map[(*f).getOpExpr()]->push_back((*f));
169 Not_replaced_set.insert(*f);
171 Expr NewValue = name_map.find(pair<Expr, Expr> (
172 (*f).getOpExpr(), (*f)))->second;
173 Expr Add = ITE_generator((*f), NewValue, Creation_map,
175 ITE_map.insert(pair<Expr, Expr> ((*f), Add));
176 Creation_map[(*f).getOpExpr()]->push_back((*f));
185 void ExprTransform::RemoveFunctionApps(
const Expr& orig, set<Expr>& Not_replaced_set, vector<Expr>& Old, vector<Expr>& New,
T_ITE_map& ITE_map, set<Expr>& SeenBefore) {
186 if (!SeenBefore.insert( orig ).second)
189 for (
int i = 0; i < orig.
arity() ; i++)
190 RemoveFunctionApps(orig[i], Not_replaced_set, Old, New, ITE_map, SeenBefore);
191 if (orig.
isApply() && orig.
getOpKind() ==
UFUNC && Not_replaced_set.find(orig) != Not_replaced_set.end()) {
193 New.push_back(ITE_map.find(orig)->second);
199 void ExprTransform::GetSortedOpVec(
B_Term_map& X_generator_map,
B_Term_map& X_term_map,
B_Term_map& P_term_map, set<Expr>& P_terms, set<Expr>& G_terms, set<Expr>& X_terms, vector<Expr>& sortedOps, set<Expr>& SeenBefore) {
201 for (B_Term_map::iterator i = X_generator_map.begin(); i != X_generator_map.end(); i++) {
203 for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
204 if (P_terms.find(*j) != P_terms.end()) {
205 vector<Expr>::iterator k = j;
208 for (; k != (*i).second->end(); k++) {
209 if (G_terms.find(*k) != G_terms.end() && !added) {
210 if (X_term_map.find((*j).getOpExpr()) == X_term_map.end())
211 X_term_map.insert(pair<
Expr, vector<Expr>*>((*j).getOpExpr(),
new vector<Expr>));
212 X_term_map[(*j).getOpExpr()]->push_back(*j);
224 map<int, set<Expr>*> Opmap;
225 for (B_Term_map::iterator i = P_term_map.begin(); i != P_term_map.end(); i++) {
227 for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++)
229 if (X_term_map.find((*i).first) != X_term_map.end()) {
230 for (vector<Expr>::iterator j = X_term_map[(*i).first]->begin(); j != X_term_map[(*i).first]->end(); j++)
233 if (Opmap.find(count) == Opmap.end())
234 Opmap.insert(pair<
int, set<Expr>*>(count,
new set<Expr>));
235 Opmap[count]->insert((*i).first);
236 sorted.insert(count);
238 vector<int> sortedvec;
239 for (set<int>::iterator i = sorted.begin(); i != sorted.end(); i++)
240 sortedvec.push_back(*i);
241 sort(sortedvec.begin(), sortedvec.end());
244 for (vector<int>::iterator i = sortedvec.begin(); i != sortedvec.end(); i++) {
245 for (set<Expr>::iterator j = Opmap[*i]->begin(); j != Opmap[*i]->end(); j++)
246 sortedOps.push_back(*j);
252 void ExprTransform::GetFormulaMap(
const Expr& e, set<Expr>& formula_map, set<Expr>& G_terms,
int& size,
int negations) {
253 if (e.
isEq() && negations % 2 == 1)
254 formula_map.insert(e);
258 for (
int i = 0; i < e.
arity(); i++)
259 GetFormulaMap(e[i], formula_map, G_terms, size, negations);
262 void ExprTransform::GetGTerms2(set<Expr>& formula_map, set<Expr>& G_terms) {
264 for (set<Expr>::iterator i = formula_map.begin(); i != formula_map.end(); i++)
265 if ((*i)[0].isTerm())
266 for (
int j = 0; j < 2; j++) {
267 G_terms.insert((*i)[j]);
271 void ExprTransform::GetSub_vec(
T_ITE_vec& ITE_vec,
const Expr& e, set<Expr>& ITE_Added) {
273 for (
int i = 0; i < e.
arity(); i++ )
274 GetSub_vec(ITE_vec, e[i], ITE_Added);
275 if (e.
isTerm() && ITE_Added.insert(e).second)
276 ITE_vec.push_back(e);
281 void ExprTransform::GetOrderedTerms(
B_formula_map& instance_map,
B_name_map& name_map,
B_Term_map& X_term_map,
T_ITE_vec& ITE_vec, set<Expr>& G_terms, set<Expr>& X_terms, vector<Expr>& Pred_vec, vector<Expr>& sortedOps, vector<Expr>& Constrained_vec, vector<Expr>& UnConstrained_vec, set<Expr>& Constrained_set, set<Expr>& UnConstrained_set,
B_Term_map& G_term_map,
B_Term_map& P_term_map, set<Expr>& SeenBefore, set<Expr>& ITE_Added) {
284 for (vector<Expr>::iterator i = sortedOps.begin(); i != sortedOps.end(); i++){
285 if (G_term_map.find(*i) != G_term_map.end()) {
286 for (vector<Expr>::iterator j = G_term_map[*i]->begin(); j != G_term_map[*i]->end(); j++)
287 GetSub_vec(ITE_vec,(*j), ITE_Added);
290 for (vector<Expr>::iterator i = sortedOps.begin(); i != sortedOps.end(); i++){
291 if (!P_term_map[*i]->empty()) {
292 for (vector<Expr>::iterator j = P_term_map[*i]->begin(); j != P_term_map[*i]->end(); j++)
293 GetSub_vec(ITE_vec, (*j), ITE_Added);
296 for (vector<Expr>::iterator i = ITE_vec.begin(); i != ITE_vec.end(); i++) {
297 if (G_terms.find(*i) != G_terms.end()) {
298 UnConstrained_set.insert(*i);
299 UnConstrained_vec.push_back(*i);
301 else if ((*i).isApply()) {
302 if (instance_map[(*i).getOpExpr()] > 40){
303 UnConstrained_set.insert(*i);
304 UnConstrained_vec.push_back(*i);
306 }
else if (X_terms.find(*i) == X_terms.end()) {
307 Constrained_set.insert(*i);
308 Constrained_vec.push_back(*i);
311 vector<Expr>::iterator j = i;
314 for (; j != ITE_vec.end(); j++) {
316 if (G_terms.find(*j) != G_terms.end() && (*j).getOpExpr() == (*i).getOpExpr() && !found) {
317 UnConstrained_vec.push_back(*i);
318 UnConstrained_set.insert(*i);
325 Constrained_vec.push_back(*i);
326 Constrained_set.insert(*i);
332 for (vector<Expr>::iterator l = Pred_vec.begin(); l != Pred_vec.end(); l++)
333 ITE_vec.push_back(*l);
343 B_type_map& type_map, vector<Expr>& Pred_vec, set<Expr>& P_terms, set<Expr>& G_terms,
345 if ( !SeenBefore.insert( e ).second )
349 if ( generator_map.find( e.
getOpExpr() ) == generator_map.end() )
350 generator_map.insert(pair<
Expr, set<Expr>* >( e.
getOpExpr(),
new set<Expr>()));
354 Pred_vec.push_back(e);
355 for (
int i = 0; i < e.
arity(); i++ )
356 BuildBryantMaps(e[i], generator_map, X_generator_map, type_map, Pred_vec, P_terms, G_terms, P_term_map, G_term_map, SeenBefore, ITE_Added);
359 if (e.
isTerm() && G_terms.find(e) == G_terms.end())
364 if (X_generator_map.find(e.
getOpExpr()) == X_generator_map.end())
365 X_generator_map.insert(pair<
Expr, vector<Expr>* >( e.
getOpExpr(),
new vector<Expr>()));
366 X_generator_map[e.
getOpExpr()]->push_back(e);
368 if (ITE_Added.insert(e).second) {
369 if (G_terms.find(e) != G_terms.end()) {
371 G_term_map.insert(pair<
Expr, vector<Expr>*>(e,
new vector<Expr>()));
372 P_term_map.insert(pair<
Expr, vector<Expr>*>(e,
new vector<Expr>()));
373 G_term_map[e]->push_back(e);
377 if (G_term_map.find(e.
getOpExpr()) == G_term_map.end()) {
378 G_term_map.insert(pair<
Expr, vector<Expr>*>(e.
getOpExpr(),
new vector<Expr>()));
379 P_term_map.insert(pair<
Expr, vector<Expr>*>(e.
getOpExpr(),
new vector<Expr>()));
386 if (P_term_map.find(e) == P_term_map.end())
387 P_term_map.insert(pair<
Expr, vector<Expr>*>(e,
new vector<Expr>()));
388 P_term_map[e]->push_back(e);
391 if (P_term_map.find(e.
getOpExpr()) == P_term_map.end())
392 P_term_map.insert(pair<
Expr, vector<Expr>*>(e.
getOpExpr(),
new vector<Expr>()));
401 void ExprTransform::GetPEqs(
const Expr& e,
B_name_map& name_map, set<Expr>& P_constrained_set, set<Expr>& Constrained_set,
T_generator_map& Constrained_map, set<Expr>& SeenBefore) {
402 if (!SeenBefore.insert(e).second)
405 if (Constrained_set.find(e[1]) != Constrained_set.end()
406 && Constrained_set.find(e[0]) != Constrained_set.end()) {
412 Temp0 = name_map.find(pair<Expr, Expr> ((e[0]).getOpExpr(),
417 Temp1 = name_map.find(pair<Expr, Expr> ((e[1]).getOpExpr(),
423 if (P_constrained_set.find(Reflexor) == P_constrained_set.end())
424 P_constrained_set.insert(Eq);
426 }
else if (Constrained_set.find(e[0]) != Constrained_set.end()) {
427 if (Constrained_map.find(e[0]) == Constrained_map.end())
428 Constrained_map.insert(pair<
Expr, set<Expr>*> (e[0],
new set<
430 Constrained_map[e[0]]->insert(e[1]);
431 }
else if (Constrained_set.find(e[1]) != Constrained_set.end()) {
432 if (Constrained_map.find(e[1]) == Constrained_map.end())
433 Constrained_map.insert(pair<
Expr, set<Expr>*> (e[1],
new set<
435 Constrained_map[e[1]]->insert(e[0]);
438 for (
int i = 0; i < e.
arity(); i++)
439 GetPEqs(e[i], name_map, P_constrained_set, Constrained_set, Constrained_map, SeenBefore);
442 Expr ExprTransform::ConstrainedConstraints(set<Expr>& Not_replaced_set,
T_generator_map& Constrained_map,
B_name_map& name_map,
B_Term_map& Creation_map, set<Expr>& Constrained_set, set<Expr>& UnConstrained_set, set<Expr>& P_constrained_set) {
443 if (Constrained_set.empty())
444 return d_core->trueExpr();
447 for (T_generator_map::iterator f = Constrained_map.begin(); f != Constrained_map.end(); f++) {
450 if ((*f).first.isVar())
453 Value = name_map.find(pair<Expr, Expr>((*f).first.getOpExpr(),(*f).first))->second;
454 for (set<Expr>::iterator j = (*f).second->begin(); j != (*f).second->end(); j++) {
456 if ((*j).isVar() || Not_replaced_set.find(*j) != Not_replaced_set.end()){
459 P_constrained_set.insert(Temp);
462 vector<Expr>::iterator c = Creation_map[(*j).getOpExpr()]->begin();
464 while ( !done && c != Creation_map[(*j).getOpExpr()]->end() ) {
467 Expr Temp = name_map.find(pair<Expr, Expr>((*c).getOpExpr(),(*c)))->second;
469 TempEqExpr = TempEqExpr.
notExpr();
471 P_constrained_set.insert(TempEqExpr);
479 if (P_constrained_set.empty())
480 return d_core->trueExpr();
482 Expr Constraints = *(P_constrained_set.begin());
483 set<Expr>::iterator i = P_constrained_set.begin();
485 for (; i != P_constrained_set.end(); i++)
486 Constraints = Constraints.
andExpr(*i);
495 for (B_Term_map::iterator i = X_generator_map.begin(); i != X_generator_map.end(); i++) {
496 map<int, vector<Expr>*> Order_map;
498 for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
500 int Counter = CountSubTerms(*j, temp);
501 if (Order_map.find(Counter) == Order_map.end())
502 Order_map.insert(pair<
int, vector<Expr>*>(Counter,
new vector<Expr>));
503 Order_map[Counter]->push_back(*j);
504 Order_set.insert(Counter);
506 vector<int> Order_vec;
507 for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
508 Order_vec.push_back(*m);
509 (*i).second->clear();
510 sort(Order_vec.begin(), Order_vec.end());
511 for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
512 for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
513 (*i).second->push_back(*l);
518 for (B_Term_map::iterator i = G_term_map.begin(); i != G_term_map.end(); i++) {
519 map<int, vector<Expr>*> Order_map;
521 for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
523 int Counter = CountSubTerms(*j, temp);
524 if (Order_map.find(Counter) == Order_map.end())
525 Order_map.insert(pair<
int, vector<Expr>*>(Counter,
new vector<Expr>));
526 Order_map[Counter]->push_back(*j);
527 Order_set.insert(Counter);
529 vector<int> Order_vec;
530 for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
531 Order_vec.push_back(*m);
532 (*i).second->clear();
533 sort(Order_vec.begin(), Order_vec.end());
534 for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
535 for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
536 (*i).second->push_back(*l);
540 for (B_Term_map::iterator i = P_term_map.begin(); i != P_term_map.end(); i++) {
541 map<int, vector<Expr>*> Order_map;
543 for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
545 int Counter = CountSubTerms(*j, temp);
546 if (Order_map.find(Counter) == Order_map.end())
547 Order_map.insert(pair<
int, vector<Expr>*>(Counter,
new vector<Expr>));
548 Order_map[Counter]->push_back(*j);
549 Order_set.insert(Counter);
551 vector<int> Order_vec;
552 for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
553 Order_vec.push_back(*m);
554 (*i).second->clear();
555 sort(Order_vec.begin(), Order_vec.end());
556 for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
557 for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
558 (*i).second->push_back(*l);
564 for (B_Term_map::iterator j = Map.begin(); j != Map.end(); j++)
569 for (T_generator_map::iterator j = Map.begin(); j != Map.end(); j++)
576 set<Expr> P_terms, G_terms, X_terms, formula_1_map, Constrained_set, UnConstrained_set, P_constrained_set, UnConstrained_Pred_set, Not_replaced_set;
579 B_Term_map P_term_map, G_term_map, X_term_map, X_generator_map, Creation_map;
585 GetFormulaMap(U, formula_1_map, G_terms, size, 0);
588 GetGTerms2(formula_1_map, G_terms);
589 vector<Expr> sortedOps, Constrained_vec, UnConstrained_vec, Pred_vec;
590 set<Expr> SeenBefore1, ITE_Added1;
591 BuildBryantMaps(U, generator_map, X_generator_map, type_map, Pred_vec, P_terms, G_terms, P_term_map, G_term_map, SeenBefore1, ITE_Added1);
592 bool proceed =
false;
593 for (T_generator_map::iterator i = generator_map.begin(); i != generator_map.end(); i++)
594 if ((*i).second->begin()->isTerm()) {
597 for (set<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++)
601 instance_map.insert(pair<Expr, int>((*i).first, count));
606 return d_core->reflexivityRule(T);
609 GetOrdering(X_generator_map, G_term_map, P_term_map);
610 name_map = BryantNames(generator_map, type_map);
611 set<Expr> SeenBefore2;
612 GetSortedOpVec(X_generator_map, X_term_map, P_term_map, P_terms, G_terms, X_terms, sortedOps, SeenBefore2);
613 set<Expr> SeenBefore3, ITE_added3;
614 GetOrderedTerms(instance_map, name_map, X_term_map, ITE_vec, G_terms, X_terms, Pred_vec, sortedOps, Constrained_vec, UnConstrained_vec, Constrained_set, UnConstrained_set, G_term_map, P_term_map, SeenBefore3, ITE_added3);
621 Get_ITEs(instance_map, Not_replaced_set, P_term_map, ITE_vec, Creation_map, name_map, ITE_map);
623 set<Expr> SeenBefore4;
624 GetPEqs(U, name_map, P_constrained_set, Constrained_set, Constrained_map, SeenBefore4);
627 PredConstrainTester(Not_replaced_set, U, name_map, Pred_vec, Constrained_set, P_constrained_set, Constrained_map);
629 Expr Constraints = ConstrainedConstraints(Not_replaced_set, Constrained_map, name_map, Creation_map, Constrained_set, UnConstrained_set, P_constrained_set);
641 set<Expr> SeenBefore6;
643 RemoveFunctionApps(U, Not_replaced_set, Old, New, ITE_map, SeenBefore6);
651 B_Term_Map_Deleter(Creation_map);
652 B_Term_Map_Deleter(X_generator_map);
653 B_Term_Map_Deleter(X_term_map);
654 B_Term_Map_Deleter(G_term_map);
655 T_generator_Map_Deleter(Constrained_map);
656 T_generator_Map_Deleter(generator_map);
659 return d_rules->dummyTheorem(T.
iffExpr(Final));
Data structure of expressions in CVC3.
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Generic API for a validity checker.
MS C++ specific settings.
Expr eqExpr(const Expr &right) const
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Expr andExpr(const Expr &right) const
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Expr impExpr(const Expr &right) const
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Expr iffExpr(const Expr &right) const
Proof rules used by theory_core.
Expr substExpr(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
Type getType() const
Get the type. Recursively compute if necessary.