CVC Lite: circuit.cpp Source File

00001 #include "circuit.h"
00002 #include "search_fast.h"
00003 #include "search_rules.h"
00004 
00005 using namespace std;
00006 
00007 namespace CVCL
00008 {
00009 
00010 Circuit::Circuit(SearchEngineFast* se, const Theorem& thm)
00011   : d_thm(thm)
00012 {
00013   const Expr& e = d_thm.getExpr();
00014   for (int i = 0; i < e.arity(); i++)
00015   {
00016     d_lits[i] =
00017       e[i].isNot() ?
00018       Literal(Variable(se->d_vm, e[i][0]), false) :
00019       Literal(Variable(se->d_vm, e[i]), true);
00020 
00021     se->d_circuitsByExpr[e[i]].push_back(this);
00022     se->d_circuitsByExpr[e[i].negate()].push_back(this);
00023   }
00024 }
00025 
00026 #define vals3(a, b, c) ((a) + 1 + ((b) + 1) * 3 + ((c) + 1) * 9)
00027 #define vals4(a, b, c, d) (vals3(a, b, c) + ((d) + 1) * 27)
00028 
00029 bool Circuit::propagate(SearchEngineFast* se)
00030 {
00031   int v0 = d_lits[0].getValue();
00032   int v1 = d_lits[1].getValue();
00033   int v2 = d_lits[2].getValue();
00034   int v3 = d_lits[3].getValue();
00035 
00036   const Theorem& t0 = d_lits[0].getTheorem();
00037   const Theorem& t1 = d_lits[1].getTheorem();
00038   const Theorem& t2 = d_lits[2].getTheorem();
00039   const Theorem& t3 = d_lits[3].getTheorem();
00040 
00041   int values = d_thm.getExpr().arity() == 3 ?
00042     vals3(v0, v1, v2) : vals4(v0, v1, v2, v3);
00043 
00044   Theorem thm;
00045   Theorem thm2;
00046 
00047   switch (d_thm.getExpr().getKind())
00048   {
00049   case AND_R:
00050     switch (values)
00051     {
00052     case vals3(0,0,0): case vals3(0,0,1): case vals3(0,1,0):
00053     case vals3(1,1,1): case vals3(-1,0,0): case vals3(-1,0,-1):
00054     case vals3(-1,1,-1): case vals3(-1,-1,0): case vals3(-1,-1,1):
00055     case vals3(-1,-1,-1):
00056       break;
00057 
00058     case vals3(0,0,-1): case vals3(0,1,-1): case vals3(0,-1,0):
00059     case vals3(0,-1,1): case vals3(0,-1,-1):
00060       // simp
00061       thm = se->d_rules->propAndrAF(d_thm, v1 == -1, v1 == -1 ? t1 : t2);
00062       break;
00063 
00064     case vals3(0,1,1):
00065       // simp
00066       thm = se->d_rules->propAndrAT(d_thm, t1, t2);
00067       break;
00068 
00069     case vals3(1,1,0): case vals3(1,0,1): case vals3(1,0,0):
00070       // split cases to avoid doing extra work?
00071       se->d_rules->propAndrLRT(d_thm, t0, &thm, &thm2);
00072       break;
00073 
00074     case vals3(-1,0,1):
00075       thm = se->d_rules->propAndrLF(d_thm, t0, t2);
00076       break;
00077 
00078     case vals3(-1,1,0):
00079       thm = se->d_rules->propAndrRF(d_thm, t0, t1);
00080       break;
00081 
00082     case vals3(1,0,-1): case vals3(1,1,-1): case vals3(1,-1,0):
00083     case vals3(1,-1,1): case vals3(1,-1,-1):
00084       se->d_conflictTheorem =
00085         se->d_rules->confAndrAT(d_thm, t0, v1 == -1, v1 == -1 ? t1 : t2);
00086       return false;
00087 
00088     case vals3(-1,1,1):
00089       se->d_conflictTheorem =
00090         se->d_rules->confAndrAF(d_thm, t0, t1, t2);
00091       return false;
00092     }
00093     break;
00094 
00095   case IFF_R:
00096     switch (values)
00097     {
00098     case vals3(0,0,0): case vals3(0,0,1): case vals3(0,0,-1):
00099     case vals3(0,1,0): case vals3(0,-1,0): case vals3(1,0,0):
00100     case vals3(1,1,1): case vals3(1,-1,-1): case vals3(-1,0,0):
00101     case vals3(-1,1,-1): case vals3(-1,-1,1):
00102       break;
00103 
00104     case vals3(0,1,1): case vals3(0,-1,-1):
00105     case vals3(0,1,-1): case vals3(0,-1,1):
00106       // simp
00107       thm = se->d_rules->propIffr(d_thm, 0, t1, t2);
00108       break;
00109 
00110     case vals3(1,0,1): case vals3(-1,0,-1):
00111     case vals3(1,0,-1): case vals3(-1,0,1):
00112       thm = se->d_rules->propIffr(d_thm, 1, t0, t2);
00113       break;
00114 
00115     case vals3(1,1,0): case vals3(-1,-1,0):
00116     case vals3(1,-1,0): case vals3(-1,1,0):
00117       thm = se->d_rules->propIffr(d_thm, 2, t0, t1);
00118       break;
00119 
00120     case vals3(1,1,-1): case vals3(1,-1,1):
00121     case vals3(-1,1,1): case vals3(-1,-1,-1):
00122       se->d_conflictTheorem = se->d_rules->confIffr(d_thm, t0, t1, t2);
00123       return false;
00124     }
00125     break;
00126 
00127   case ITE_R:
00128     switch (values)
00129     {
00130     case vals4(0,0,0,0): case vals4(0,0,0,1): case vals4(0,0,0,-1):
00131     case vals4(0,0,1,0): case vals4(0,0,1,1): case vals4(0,0,1,-1):
00132     case vals4(0,0,-1,0): case vals4(0,0,-1,1): case vals4(0,0,-1,-1):
00133     case vals4(0,1,0,0): case vals4(0,1,0,1): case vals4(0,1,0,-1):
00134     case vals4(0,-1,0,0): case vals4(0,-1,1,0): case vals4(0,-1,-1,0):
00135     case vals4(1,0,0,0): case vals4(1,0,0,1): case vals4(1,0,1,0):
00136     case vals4(1,0,1,1): case vals4(1,1,1,0): case vals4(1,1,1,1):
00137     case vals4(1,1,1,-1): case vals4(1,-1,0,1): case vals4(1,-1,1,1):
00138     case vals4(1,-1,-1,1): case vals4(-1,0,0,0): case vals4(-1,0,0,-1):
00139     case vals4(-1,0,-1,0): case vals4(-1,0,-1,-1): case vals4(-1,1,-1,0):
00140     case vals4(-1,1,-1,1): case vals4(-1,1,-1,-1): case vals4(-1,-1,0,-1):
00141     case vals4(-1,-1,1,-1): case vals4(-1,-1,-1,-1):
00142       break;
00143 
00144     case vals4(0,1,1,0): case vals4(0,1,1,1): case vals4(0,1,1,-1):
00145     case vals4(0,1,-1,0): case vals4(0,1,-1,1): case vals4(0,1,-1,-1):
00146     case vals4(0,-1,0,-1): case vals4(0,-1,1,-1): case vals4(0,-1,-1,-1):
00147     case vals4(0,-1,0,1): case vals4(0,-1,1,1): case vals4(0,-1,-1,1):
00148       // simp
00149       thm = se->d_rules->propIterIte(d_thm, v1 == 1, t1, v1 == 1 ? t2 : t3);
00150       break;
00151 
00152     case vals4(1,0,0,-1): case vals4(1,0,1,-1): case vals4(1,0,-1,0):
00153     case vals4(1,0,-1,1): case vals4(-1,0,0,1): case vals4(-1,0,1,0):
00154     case vals4(-1,0,1,-1): case vals4(-1,0,-1,1):
00155       se->d_rules->propIterIfThen(d_thm, v0 == -v2, t0, v0 == -v2 ? t2 : t3,
00156                                   &thm, &thm2);
00157       break;
00158 
00159     case vals4(1,1,0,0): case vals4(1,1,0,1): case vals4(1,1,0,-1):
00160     case vals4(1,-1,0,0): case vals4(1,-1,1,0): case vals4(1,-1,-1,0):
00161     case vals4(-1,1,0,0): case vals4(-1,1,0,1): case vals4(-1,1,0,-1):
00162     case vals4(-1,-1,0,0): case vals4(-1,-1,1,0): case vals4(-1,-1,-1,0):
00163       thm = se->d_rules->propIterThen(d_thm, t0, t1);
00164       break;
00165 
00166     case vals4(1,0,-1,-1): case vals4(-1,0,1,1):
00167     case vals4(-1,1,1,1): case vals4(1,1,-1,-1):
00168       se->d_conflictTheorem =
00169         se->d_rules->confIterThenElse(d_thm, t0, t2, t3);
00170       return false;
00171 
00172     case vals4(1,1,-1,0): case vals4(1,1,-1,1): case vals4(1,-1,0,-1):
00173     case vals4(1,-1,1,-1): case vals4(1,-1,-1,-1): case vals4(-1,1,1,0):
00174     case vals4(-1,1,1,-1): case vals4(-1,-1,0,1): case vals4(-1,-1,1,1):
00175     case vals4(-1,-1,-1,1):
00176       se->d_conflictTheorem =
00177         se->d_rules->confIterIfThen(d_thm, v1 == 1, t0, t1, v1 == 1 ? t2 : t3);
00178       return false;
00179     }
00180     break;
00181 
00182   default:
00183     DebugAssert(false, "unhandled circuit");
00184   }
00185 
00186   if (!thm.isNull() && se->newLiteral(thm.getExpr()).getValue() == 0)
00187   {
00188     se->d_core->addFact(thm);
00189     se->recordFact(thm);
00190     se->d_literals.push_back(se->newLiteral(thm.getExpr()));
00191     se->d_circuitPropCount++;
00192   }
00193 
00194   if (!thm2.isNull() && se->newLiteral(thm2.getExpr()).getValue() == 0)
00195   {
00196     se->d_core->addFact(thm2);
00197     se->recordFact(thm2);
00198     se->d_literals.push_back(se->newLiteral(thm2.getExpr()));
00199     se->d_circuitPropCount++;
00200   }
00201 
00202   return true;
00203 }
00204 
00205 
00206 } // namespace CVCL
00207