Changes

3 files changed, 83 insertions, 12 deletions

diff --git a/main.cpp b/main.cpp
index 2b7e748..f4fe639 100644
--- a/main.cpp
+++ b/main.cpp
@@ -42,9 +42,8 @@ vector<Axiom> importAxioms(const vector<string> &list){
 
 using Heuristic = int (*)(const Tree&);
 
-int heuristic(const Tree &tree){
-	return tree.nleaves();
-}
+int heuristic_nleaves(const Tree &tree){return tree.nleaves();}
+int heuristic_height(const Tree &tree){return tree.height();}
 
 template <Heuristic F>
 struct AscendingCompare{
@@ -99,25 +98,43 @@ vector<Tree>* deduceEq(const vector<Axiom> &axioms,const Tree &startTree,const T
 }
 
 
+void test_func(){
+	Tree from("([2]*([2]*1))"),to("10");
+	Tree subj("(([1]*1)*[1])");
+
+	/*unordered_set<Variable> temps=to.collectTemporaries();
+	for(Variable v : temps){
+		cout<<v<<endl;
+	}*/
+
+	vector<Tree> res=subj.replace(from,to);
+	for(const Tree &t : res){
+		cout<<t<<endl;
+	}
+}
+
 int main(){
+	test_func();
+	return 0;
+
 	const vector<Axiom> axioms=importAxioms({
-		// "([1]*[2])>([2]*[1])",
-		// "(([1]*[2])*[3])=([1]*([2]*[3]))",
+		// "([1]*[2])>([2]*[1])",  // Commutativity
+		// "(([1]*[2])*[3])=([1]*([2]*[3]))",  // Associativity
 
-		// "([1]*([1]*[2]))=[1]",
-		// "(([2]*[1])*[1])=[1]",
+		"([1]*([1]*[2]))=[1]",  // Onno's 1=2 axioms
+		"(([2]*[1])*[1])=[1]",
 
 		// "[1]=([1]*[1])",
 		// "(([1]*[2])*[3])=(([2]*[3])*[1])",
 
-		"[1]=[2]",
+		// "[1]=[2]",
 	});
-	const Tree t_from("(1*2)"),t_to("(2*1)");
+	const Tree t_from("1"),t_to("2");
 
 	for(const Axiom &ax : axioms)cout<<ax<<endl;
 	cout<<endl;
 
-	vector<Tree> *res=deduceEq<heuristic>(axioms,t_from,t_to);
+	vector<Tree> *res=deduceEq<heuristic_nleaves>(axioms,t_from,t_to);
 	if(res==nullptr){
 		cout<<"No deduction"<<endl;
 	} else {
diff --git a/tree.cpp b/tree.cpp
index 8d677db..a259e9b 100644
--- a/tree.cpp
+++ b/tree.cpp
@@ -11,6 +11,8 @@ int uniqid(){
 }
 
 
+Variable::Variable(int id):id(id){}
+
 bool Variable::isOperator() const {
 	return id==0;
 }
@@ -167,6 +169,15 @@ Tree::Node* Tree::Node::apply(const Assign &as) const {
 	return n;
 }
 
+void Tree::Node::collectTemporaries(unordered_set<Variable> &accum) const {
+	if(v.isOperator()){
+		left->collectTemporaries(accum);
+		right->collectTemporaries(accum);
+	} else {
+		accum.insert(v);
+	}
+}
+
 int Tree::Node::nleaves() const {
 	if(v.isOperator()){
 		return left->nleaves()+right->nleaves();
@@ -175,6 +186,11 @@ int Tree::Node::nleaves() const {
 	}
 }
 
+int Tree::Node::height() const {
+	if(v.isOperator())return max(left->height(),right->height());
+	else return 1;
+}
+
 int Tree::Node::compare(const Node &other) const {
 	if(v.isTemp()&&other.v.isTemp())return 0;
 	if(v<other.v)return -1;
@@ -283,9 +299,27 @@ bool Tree::matches(const Tree &pat) const {
 	}
 }
 
+void Tree::refreshUnassigned(const Tree &repl,Assign &as) const {
+	unordered_set<Variable> temps=repl.collectTemporaries();
+	// cerr<<"rU:"<<endl;
+	for(Variable v : temps){
+		// cerr<<"  v = "<<v<<endl;
+		if(v.isTemp()&&as.find(v)==as.end()){
+			int id=uniqid();
+			as.emplace(v,Node(id));
+			// cerr<<"  emplace("<<v<<","<<Node(id)<<")"<<endl;
+		}
+	}
+}
+
 void Tree::replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &accum){
 	Assign *as=subj->match(*pat.root);
 	if(as){
+		refreshUnassigned(repl,*as);
+		cerr<<"replace("<<*subj<<","<<pat<<","<<repl<<"); as:"<<endl;
+		for(const pair<Variable,Node> &p : *as){
+			cerr<<"  "<<p.first<<" -> "<<p.second<<endl;
+		}
 		Node *res=repl.root->apply(*as);
 		Node backup=*subj;
 		*subj=*res;
@@ -307,11 +341,23 @@ vector<Tree> Tree::replace(const Tree &pat,const Tree &repl){
 	return res;
 }
 
+unordered_set<Variable> Tree::collectTemporaries() const {
+	assert(root);
+	unordered_set<Variable> temps;
+	root->collectTemporaries(temps);
+	return temps;
+}
+
 int Tree::nleaves() const {
 	assert(root);
 	return root->nleaves();
 }
 
+int Tree::height() const {
+	assert(root);
+	return root->height();
+}
+
 int Tree::compare(const Tree &other) const {
 	assert(root&&other.root);
 	return root->compare(*other.root);
diff --git a/tree.h b/tree.h
index 7d8cf15..5f008d7 100644
--- a/tree.h
+++ b/tree.h
@@ -4,6 +4,7 @@
 #include <string>
 #include <vector>
 #include <unordered_map>
+#include <unordered_set>
 
 using namespace std;
 
@@ -13,7 +14,7 @@ int uniqid();
 struct Variable{
 	int id;
 
-	Variable(int id):id(id){}
+	Variable(int id);
 
 	bool isOperator() const;
 	bool isFixed() const;
@@ -25,6 +26,8 @@ struct Variable{
 	operator int() const;
 };
 
+ostream& operator<<(ostream &os,const Variable &v);
+
 namespace std {
 	template <>
 	struct hash<Variable>{
@@ -50,10 +53,11 @@ class Tree{
 		Node& operator=(const Node &other);
 
 		Assign* match(const Node &pat,Assign *accum=nullptr) const;
-
 		Node* apply(const Assign &as) const;
+		void collectTemporaries(unordered_set<Variable> &accum) const;
 
 		int nleaves() const;
+		int height() const;
 
 		int compare(const Node &other) const;
 	};
@@ -65,6 +69,8 @@ class Tree{
 
 	void replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &accum);
 
+	void refreshUnassigned(const Tree &repl,Assign &as) const;
+
 public:
 	Tree(); // Creates invalid tree
 	Tree(const string &expr);
@@ -75,8 +81,10 @@ public:
 
 	bool matches(const Tree &pat) const;
 	vector<Tree> replace(const Tree &pat,const Tree &repl);
+	unordered_set<Variable> collectTemporaries() const;
 
 	int nleaves() const;
+	int height() const;
 
 	int compare(const Tree &other) const;