Skip to content

Commit

Permalink
Implement different version of proof production with long transitivit…
Browse files Browse the repository at this point in the history 
…y chains and experiment with R.apply
  • Loading branch information
@AFellner
AFellner committed May 6, 2014
1 parent cb973ea commit dfaec82
Show file tree
Hide file tree
Showing 12 changed files with 666 additions and 427 deletions.
31 changes: 16 additions & 15 deletions src/main/scala/at/logic/skeptik/algorithm/congruence/Congruence.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import at.logic.skeptik.expression.formula._
import at.logic.skeptik.algorithm.dijkstra._
//import scala.collection.mutable.{HashMap => MMap}
import scala.collection.immutable.{HashMap => IMap}
import scala.collection.mutable.{HashMap => MMap}
import scala.collection.mutable.Stack
import scala.collection.immutable.Queue
import scala.collection.mutable.ListBuffer
Expand All @@ -19,9 +20,9 @@ import scala.collection.mutable.ListBuffer
//bla[PathTree[E,]]

class Congruence(
val eqReferences: MMap[(E,E),App],
val find: FindTable = new FindTable(),
val sigTable: SignatureTable = new SignatureTable(),
val eqReferences: IMap[(E,E),App] = new IMap[(E,E),App],
val deduced: Queue[(E,E)] = Queue[(E,E)](),
val g: WGraph[E,EqLabel] = new WGraph[E,EqLabel]()) {

Expand All @@ -36,19 +37,19 @@ class Congruence(
// def copy =

def updateFind(newFind: FindTable) = {
new Congruence(newFind, sigTable, eqReferences,deduced,g)
new Congruence(eqReferences, newFind, sigTable,deduced,g)
}
def updateSigTable(newSigTable: SignatureTable) = {
new Congruence(find, newSigTable, eqReferences,deduced,g)
}
def updateEqReferences(newEqReferences: IMap[(E,E),App]) = {
new Congruence(find, sigTable, newEqReferences,deduced,g)
new Congruence(eqReferences, find, newSigTable,deduced,g)
}
// def updateEqReferences(newEqReferences: MMap[(E,E),App]) = {
// new Congruence(find, sigTable, newEqReferences,deduced,g)
// }
def updateDeduced(newDeduced: Queue[(E,E)]) = {
new Congruence(find, sigTable, eqReferences,newDeduced,g)
new Congruence(eqReferences, find, sigTable,newDeduced,g)
}
def updateGraph(newG: WGraph[E,EqLabel]) = {
new Congruence(find, sigTable, eqReferences,deduced,newG)
new Congruence(eqReferences, find, sigTable,deduced,newG)
}

def addAll(eqs: List[App]): Congruence = {
Expand All @@ -57,9 +58,9 @@ class Congruence(

def addEquality(eq: App): Congruence = {
val (l,r) = (eq.function.asInstanceOf[App].argument,eq.argument)
val eqRef = eqReferences.updated((l,r), eq)
val c0 = updateEqReferences(eqRef)
val c1 = c0.addNode(l)
val eqRef = eqReferences.update((l,r), eq)
// val c0 = updateEqReferences(eqRef)
val c1 = this.addNode(l)
val c2 = c1.addNode(r)
val c3 = c2.updateGraph(c2.g.addUndirectedEdge((l,(eq,None),r), 1))
val res = c3.merge(l,r,Some(eq))
Expand Down Expand Up @@ -173,7 +174,7 @@ class Congruence(
}

def resolveDeduced(u: E, v: E): Congruence = {
val dij = new EquationDijkstra
val dij = new EquationDijkstra(eqReferences)
// println("resolve deduced: " + (u,v))
u match {
case App(u1,u2) => {
Expand All @@ -197,7 +198,7 @@ class Congruence(
// println("equations: "+ eqAll)
//if (weight > 0) here?
// if (u.t != v.t) println("Types are not the same for " + (u,v))
val x = Eq(u,v)
val x = Eq(u,v,eqReferences)
if (x.toString == "((f2 c_5 c_2) = c_3)" || x.toString == "(c_3 = (f2 c_5 c_2))") println("creating " + x + " when adding an edge to graph")
updateGraph(g.addUndirectedEdge((u,(x,Some(path1,path2)),v), weight))
}
Expand All @@ -207,10 +208,10 @@ class Congruence(
case _ => this
}
}

def explain(u: E, v: E): Option[EquationTree] = {
// resolveDeduced
val dij = new EquationDijkstra
val dij = new EquationDijkstra(eqReferences)
// val tmpEq = Eq(u,v)
// val tmpCon = addEquality(tmpEq)
// val realG = tmpCon.g.removeUndirectedEdge((u,(tmpEq,None),v))
Expand Down
63 changes: 52 additions & 11 deletions src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceCompressor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,15 +13,20 @@ import at.logic.skeptik.algorithm.compressor._
import at.logic.skeptik.exporter.Exporter
import at.logic.skeptik.exporter.skeptik.{FileExporter => SkeptikFileExporter}
import at.logic.skeptik.exporter.smt.{FileExporter => SMTFileExporter}
import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent}

import scala.collection.mutable.{HashMap => MMap}
import scala.collection.immutable.{HashMap => IMap}

object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes {

def apply(proof: Proof[N]): Proof[N] = {
val (con,eqNodesLeft,eqNodesRight,allEqReferences) = buildGlobalCongruence(proof)

val references = MMap[(E,E),App]()
val (con,eqNodesLeft,eqNodesRight) = buildGlobalCongruence(proof,references)
// val allEqReferences: MMap[(E,E),App] = MMap[(E,E),App]() ++ allEqReferencesImmutable
println("all references size: " + references.size)
// val istherealready = allEqReferences.values.find(p => {(p.toString == "((f1 c_3 c_3) = (f1 (f3 c6) (f3 c7)))" || p.toString == "((f1 (f3 c6) (f3 c7)) = (f1 c_3 c_3))") })
// println("is there alreay?: " + istherealready)
val premiseAxiomMap = MMap[N,Set[App]]()
// var first = true
def replaceRedundant(node: N, fromPremises: Seq[(N,Set[App],Boolean)]): (N,Set[App],Boolean) = {
Expand Down Expand Up @@ -77,14 +82,47 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes {
val path = tree.get
// println("proofing " + (path.firstVert,path.lastVert) + " from " + path.originalEqs)
// println("path: " + path)
val eqRef = con.eqReferences
// val eqRef = con.eqReferences
val pathProof = try {
path.toProof(allEqReferences)
println("TO PROOF with " + references + " references")
path.toProof(references)
}
catch {
case e: Exception => {
val exporter = new SMTFileExporter("experiments/congruence/resolveBug4")
exporter.write(Proof(fixedNodeInit))
val exporter = new SMTFileExporter("experiments/congruence/resolveBug11",true)
val origEqs = path.originalEqs
val rightSideEq = fixedNodeInit.conclusion.suc.find(expr => if (Eq.?:(expr)) origEqs.contains(expr.asInstanceOf[App]) else false)
val res1 = rightSideEq match{
case Some(eq) => {
// println(eq + " is rsEq")
R(new Axiom(new Sequent(origEqs.toSeq,Seq())),fixedNodeInit)
}
case None => {
val leftSideEq = fixedNodeInit.conclusion.ant.find(expr => if (expr.isInstanceOf[App]) origEqs.contains(expr.asInstanceOf[App]) else false)
leftSideEq match{
case Some(eq) => {
// println(eq + " is lsEq")
R(new Axiom(new Sequent(Seq(),origEqs.toSeq)),fixedNodeInit)
}
case None => {
throw new Exception("fixedNode empty? " + fixedNodeInit)
}
}
}
}
val res2 = origEqs.foldLeft(res1)({(A,B) =>
val ax = new Axiom(new Sequent(Seq(),Seq(B)))
if (A.conclusion.ant.contains(B)) R(A,ax)
else A
// try R(A,ax)
// catch {
// case e: Exception => {
// A
// }
// }
})
exporter.write(Proof(res2.asInstanceOf[N]))

exporter.flush
exporter.close
throw(e)
Expand Down Expand Up @@ -140,10 +178,8 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes {
DAGify(resProof)
}



def buildGlobalCongruence(proof: Proof[N]): (Congruence,MMap[App,N],MMap[App,N],IMap[(E,E),App]) = {
var con = new Congruence
def buildGlobalCongruence(proof: Proof[N], references: MMap[(E,E),App]): (Congruence,MMap[App,N],MMap[App,N]) = {
var con = new Congruence(references)
val eqNodesLeft = MMap[App,N]()
val eqNodesRight = MMap[App,N]()

Expand All @@ -164,6 +200,11 @@ def buildGlobalCongruence(proof: Proof[N]): (Congruence,MMap[App,N],MMap[App,N],
val leftEqs = node.conclusion.ant.filter(Eq.?:(_)).map(f => f.asInstanceOf[App])

val bothEqs = rightEqs ++ leftEqs
bothEqs.foreach(eq => {
val (l,r) = (eq.function.asInstanceOf[App].argument,eq.argument)
references += ((l,r) -> eq)
references += ((r,l) -> eq)
})
val eqMap = bothEqs.foldLeft(premiseMap)({(A,B) =>
A.updated((B.function.asInstanceOf[App].argument,B.argument), B)
})
Expand Down Expand Up @@ -200,6 +241,6 @@ def buildGlobalCongruence(proof: Proof[N]): (Congruence,MMap[App,N],MMap[App,N],
val (_,_,mapRes) = proof foldDown traverse
con = con.resolveDeducedQueue
println("eqNodesLeft in bGC " + eqNodesLeft.mkString(","))
(con,eqNodesLeft,eqNodesRight,mapRes)
(con,eqNodesLeft,eqNodesRight)
}
}
6 changes: 3 additions & 3 deletions src/main/scala/at/logic/skeptik/algorithm/dijkstra/Dijkstra.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ import at.logic.skeptik.expression._
import scala.collection.mutable.{HashSet => MSet}
import at.logic.skeptik.expression.formula._

class EquationDijkstra extends Dijkstra[E,EqLabel] {
class EquationDijkstra(references: MMap[(E,E),App]) extends Dijkstra[E,EqLabel](references) {

def pi(u: E): EquationTree = {
pathTrees.getOrElseUpdate(u,new EquationTree(u,None))
Expand All @@ -24,7 +24,7 @@ class EquationDijkstra extends Dijkstra[E,EqLabel] {
// }
}

abstract class Dijkstra[T1,T2] {
abstract class Dijkstra[T1,T2](references: MMap[(E,E),App]) {

val distances = MMap[T1,Int]()
val pathTrees = MMap[T1,EquationTree]()
Expand Down Expand Up @@ -52,7 +52,7 @@ abstract class Dijkstra[T1,T2] {
if (s == target && s.isInstanceOf[E]) {
val sE = s.asInstanceOf[E]
val end = new EquationTree(sE,None)
val x = Eq(sE,sE)
val x = Eq(sE,sE,references)
if (x.toString == "((f2 c_5 c_2) = c_3)" || x.toString == "(c_3 = (f2 c_5 c_2))") println("creating " + x + " when shortest path between two equal expr is asked")
val eqTreeEdge = new EqTreeEdge(end,(x,None))
new EquationTree(sE,Some(eqTreeEdge))
Expand Down
Loading

0 comments on commit dfaec82

Please sign in to comment.